Metamath Proof Explorer

Theorem satf0suclem

Description: Lemma for satf0suc , sat1el2xp and fmlasuc0 . (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion satf0suclem ⊢X∈U∧Y∈V∧Z∈W→xy|y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V

Proof

Step Hyp Ref Expression
1 peano1 ⊢∅∈ω
2 eleq1 ⊢y=∅→y∈ω↔∅∈ω
3 1 2 mpbiri ⊢y=∅→y∈ω
4 3 adantr ⊢y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C→y∈ω
5 4 pm4.71ri ⊢y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C↔y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C
6 5 opabbii ⊢xy|y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C=xy|y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C
7 omex ⊢ω∈V
8 7 a1i ⊢X∈U∧Y∈V∧Z∈W→ω∈V
9 simp1 ⊢X∈U∧Y∈V∧Z∈W→X∈U
10 unab ⊢x|∃v∈Yx=B∪x|∃w∈Zx=C=x|∃v∈Yx=B∨∃w∈Zx=C
11 abrexexg ⊢Y∈V→x|∃v∈Yx=B∈V
12 11 3ad2ant2 ⊢X∈U∧Y∈V∧Z∈W→x|∃v∈Yx=B∈V
13 abrexexg ⊢Z∈W→x|∃w∈Zx=C∈V
14 13 3ad2ant3 ⊢X∈U∧Y∈V∧Z∈W→x|∃w∈Zx=C∈V
15 unexg ⊢x|∃v∈Yx=B∈V∧x|∃w∈Zx=C∈V→x|∃v∈Yx=B∪x|∃w∈Zx=C∈V
16 12 14 15 syl2anc ⊢X∈U∧Y∈V∧Z∈W→x|∃v∈Yx=B∪x|∃w∈Zx=C∈V
17 10 16 eqeltrrid ⊢X∈U∧Y∈V∧Z∈W→x|∃v∈Yx=B∨∃w∈Zx=C∈V
18 17 ralrimivw ⊢X∈U∧Y∈V∧Z∈W→∀u∈Xx|∃v∈Yx=B∨∃w∈Zx=C∈V
19 abrexex2g ⊢X∈U∧∀u∈Xx|∃v∈Yx=B∨∃w∈Zx=C∈V→x|∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V
20 9 18 19 syl2anc ⊢X∈U∧Y∈V∧Z∈W→x|∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V
21 20 adantr ⊢X∈U∧Y∈V∧Z∈W∧y∈ω→x|∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V
22 8 21 opabex3rd ⊢X∈U∧Y∈V∧Z∈W→xy|y∈ω∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V
23 simpr ⊢y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C→∃u∈X∃v∈Yx=B∨∃w∈Zx=C
24 23 anim2i ⊢y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C→y∈ω∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C
25 24 ssopab2i ⊢xy|y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C⊆xy|y∈ω∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C
26 25 a1i ⊢X∈U∧Y∈V∧Z∈W→xy|y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C⊆xy|y∈ω∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C
27 22 26 ssexd ⊢X∈U∧Y∈V∧Z∈W→xy|y∈ω∧y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V
28 6 27 eqeltrid ⊢X∈U∧Y∈V∧Z∈W→xy|y=∅∧∃u∈X∃v∈Yx=B∨∃w∈Zx=C∈V