This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem satf0suclem

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

Ref Expression
Assertion satf0suclem ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) } ∈ V )

Proof

Step Hyp Ref Expression
1 peano1 ⊢ ∅ ∈ ω
2 eleq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ ω ↔ ∅ ∈ ω ) )
3 1 2 mpbiri ⊢ ( 𝑦 = ∅ → 𝑦 ∈ ω )
4 3 adantr ⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) → 𝑦 ∈ ω )
5 4 pm4.71ri ⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ↔ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) )
6 5 opabbii ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) }
7 omex ⊢ ω ∈ V
8 7 a1i ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ω ∈ V )
9 simp1 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑋 ∈ 𝑈 )
10 unab ⊢ ( { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∪ { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ) = { 𝑥 ∣ ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) }
11 abrexexg ⊢ ( 𝑌 ∈ 𝑉 → { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∈ V )
12 11 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∈ V )
13 abrexexg ⊢ ( 𝑍 ∈ 𝑊 → { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ∈ V )
14 13 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ∈ V )
15 unexg ⊢ ( ( { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∈ V ∧ { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ∈ V ) → ( { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∪ { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ) ∈ V )
16 12 14 15 syl2anc ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( { 𝑥 ∣ ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 } ∪ { 𝑥 ∣ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 } ) ∈ V )
17 10 16 eqeltrrid ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V )
18 17 ralrimivw ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ∀ 𝑢 ∈ 𝑋 { 𝑥 ∣ ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V )
19 abrexex2g ⊢ ( ( 𝑋 ∈ 𝑈 ∧ ∀ 𝑢 ∈ 𝑋 { 𝑥 ∣ ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V ) → { 𝑥 ∣ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V )
20 9 18 19 syl2anc ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑥 ∣ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V )
21 20 adantr ⊢ ( ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ 𝑦 ∈ ω ) → { 𝑥 ∣ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) } ∈ V )
22 8 21 opabex3rd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) } ∈ V )
23 simpr ⊢ ( ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) → ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) )
24 23 anim2i ⊢ ( ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) → ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) )
25 24 ssopab2i ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) }
26 25 a1i ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) } )
27 22 26 ssexd ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 ∈ ω ∧ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) ) } ∈ V )
28 6 27 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑋 ( ∃ 𝑣 ∈ 𝑌 𝑥 = 𝐵 ∨ ∃ 𝑤 ∈ 𝑍 𝑥 = 𝐶 ) ) } ∈ V )