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 → x y | y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = 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 ∈ Y x = B ∨ ∃ w ∈ Z x = C → y ∈ ω
5 4 pm4.71ri ⊢ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ↔ y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
6 5 opabbii ⊢ x y | y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C = x y | y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = 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 ∈ Y x = B ∪ x | ∃ w ∈ Z x = C = x | ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
11 abrexexg ⊢ Y ∈ V → x | ∃ v ∈ Y x = B ∈ V
12 11 3ad2ant2 ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x | ∃ v ∈ Y x = B ∈ V
13 abrexexg ⊢ Z ∈ W → x | ∃ w ∈ Z x = C ∈ V
14 13 3ad2ant3 ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x | ∃ w ∈ Z x = C ∈ V
15 unexg ⊢ x | ∃ v ∈ Y x = B ∈ V ∧ x | ∃ w ∈ Z x = C ∈ V → x | ∃ v ∈ Y x = B ∪ x | ∃ w ∈ Z x = C ∈ V
16 12 14 15 syl2anc ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x | ∃ v ∈ Y x = B ∪ x | ∃ w ∈ Z x = C ∈ V
17 10 16 eqeltrrid ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x | ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
18 17 ralrimivw ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → ∀ u ∈ X x | ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
19 abrexex2g ⊢ X ∈ U ∧ ∀ u ∈ X x | ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V → x | ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
20 9 18 19 syl2anc ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x | ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
21 20 adantr ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W ∧ y ∈ ω → x | ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
22 8 21 opabex3rd ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x y | y ∈ ω ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
23 simpr ⊢ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C → ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
24 23 anim2i ⊢ y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C → y ∈ ω ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
25 24 ssopab2i ⊢ x y | y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ⊆ x y | y ∈ ω ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
26 25 a1i ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x y | y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ⊆ x y | y ∈ ω ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C
27 22 26 ssexd ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x y | y ∈ ω ∧ y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V
28 6 27 eqeltrid ⊢ X ∈ U ∧ Y ∈ V ∧ Z ∈ W → x y | y = ∅ ∧ ∃ u ∈ X ∃ v ∈ Y x = B ∨ ∃ w ∈ Z x = C ∈ V