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 )