Metamath Proof Explorer

Theorem fiunlem

Description: Lemma for fiun and f1iun . Formerly part of f1iun . (Contributed by AV, 6-Oct-2023)

Ref Expression
Hypothesis fiun.1 ⊢ x = y → B = C
Assertion fiunlem ⊢ B : D ⟶ S ∧ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B → ∀ v ∈ z | ∃ x ∈ A z = B u ⊆ v ∨ v ⊆ u

Proof

Step Hyp Ref Expression
1 fiun.1 ⊢ x = y → B = C
2 vex ⊢ v ∈ V
3 eqeq1 ⊢ z = v → z = B ↔ v = B
4 3 rexbidv ⊢ z = v → ∃ x ∈ A z = B ↔ ∃ x ∈ A v = B
5 2 4 elab ⊢ v ∈ z | ∃ x ∈ A z = B ↔ ∃ x ∈ A v = B
6 1 eqeq2d ⊢ x = y → v = B ↔ v = C
7 6 cbvrexvw ⊢ ∃ x ∈ A v = B ↔ ∃ y ∈ A v = C
8 r19.29 ⊢ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ ∃ y ∈ A v = C → ∃ y ∈ A B ⊆ C ∨ C ⊆ B ∧ v = C
9 sseq12 ⊢ u = B ∧ v = C → u ⊆ v ↔ B ⊆ C
10 9 ancoms ⊢ v = C ∧ u = B → u ⊆ v ↔ B ⊆ C
11 sseq12 ⊢ v = C ∧ u = B → v ⊆ u ↔ C ⊆ B
12 10 11 orbi12d ⊢ v = C ∧ u = B → u ⊆ v ∨ v ⊆ u ↔ B ⊆ C ∨ C ⊆ B
13 12 biimprcd ⊢ B ⊆ C ∨ C ⊆ B → v = C ∧ u = B → u ⊆ v ∨ v ⊆ u
14 13 expdimp ⊢ B ⊆ C ∨ C ⊆ B ∧ v = C → u = B → u ⊆ v ∨ v ⊆ u
15 14 rexlimivw ⊢ ∃ y ∈ A B ⊆ C ∨ C ⊆ B ∧ v = C → u = B → u ⊆ v ∨ v ⊆ u
16 15 imp ⊢ ∃ y ∈ A B ⊆ C ∨ C ⊆ B ∧ v = C ∧ u = B → u ⊆ v ∨ v ⊆ u
17 8 16 sylan ⊢ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ ∃ y ∈ A v = C ∧ u = B → u ⊆ v ∨ v ⊆ u
18 17 an32s ⊢ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B ∧ ∃ y ∈ A v = C → u ⊆ v ∨ v ⊆ u
19 18 adantlll ⊢ B : D ⟶ S ∧ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B ∧ ∃ y ∈ A v = C → u ⊆ v ∨ v ⊆ u
20 7 19 sylan2b ⊢ B : D ⟶ S ∧ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B ∧ ∃ x ∈ A v = B → u ⊆ v ∨ v ⊆ u
21 5 20 sylan2b ⊢ B : D ⟶ S ∧ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B ∧ v ∈ z | ∃ x ∈ A z = B → u ⊆ v ∨ v ⊆ u
22 21 ralrimiva ⊢ B : D ⟶ S ∧ ∀ y ∈ A B ⊆ C ∨ C ⊆ B ∧ u = B → ∀ v ∈ z | ∃ x ∈ A z = B u ⊆ v ∨ v ⊆ u