Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι be given.
Let x3 of type ι → ι be given.
Assume H0: ∀ x4 . x4 ∈ x0 ⟶ x2 x4 ⊆ x3 x4.
Assume H1: x0 ⊆ x1.
Assume H2:
∀ x4 . x4 ∈ x1 ⟶ nIn x4 x0 ⟶ 0 ∈ x3 x4.
Apply Subq_tra with
Pi x0 (λ x4 . x2 x4),
Pi x0 (λ x4 . x3 x4),
Pi x1 (λ x4 . x3 x4) leaving 2 subgoals.
Apply Pi_cod_mon with
x0,
x2,
x3.
The subproof is completed by applying H0.
Apply Pi_0_dom_mon with
x0,
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.