satf0

Description: The satisfaction predicate as function over wff codes in the empty model with an empty binary relation. (Contributed by AV, 14-Sep-2023)

		Ref	Expression
	Assertion	satf0	⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ↾ suc ω )

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		satf	⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) )
3	1 1 2	mp2an	⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω )
4		peano1	⊢ ∅ ∈ ω
5	4	ne0ii	⊢ ω ≠ ∅
6		map0b	⊢ ( ω ≠ ∅ → ( ∅ ↑_m ω ) = ∅ )
7	5 6	ax-mp	⊢ ( ∅ ↑_m ω ) = ∅
8	7	difeq1i	⊢ ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ( ∅ ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) )
9		0dif	⊢ ( ∅ ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ∅
10	8 9	eqtri	⊢ ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) = ∅
11	10	eqeq2i	⊢ ( 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ↔ 𝑦 = ∅ )
12	11	anbi2i	⊢ ( ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) )
13	12	rexbii	⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) )
14		r19.41v	⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) )
15	13 14	bitri	⊢ ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ↔ ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) )
16	7	rabeqi	⊢ { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = { 𝑎 ∈ ∅ ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) }
17		rab0	⊢ { 𝑎 ∈ ∅ ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = ∅
18	16 17	eqtri	⊢ { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } = ∅
19	18	eqeq2i	⊢ ( 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ↔ 𝑦 = ∅ )
20	19	anbi2i	⊢ ( ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) )
21	20	rexbii	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) )
22		r19.41v	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) )
23	21 22	bitri	⊢ ( ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ↔ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) )
24	15 23	orbi12i	⊢ ( ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) )
25	24	rexbii	⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) )
26		andir	⊢ ( ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) )
27	26	bicomi	⊢ ( ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ↔ ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) )
28	27	rexbii	⊢ ( ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ∅ ) ∨ ( ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = ∅ ) ) ↔ ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) )
29		r19.41v	⊢ ( ∃ 𝑢 ∈ 𝑓 ( ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) )
30	25 28 29	3bitri	⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ∧ 𝑦 = ∅ ) )
31	30	biancomi	⊢ ( ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) )
32	31	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) }
33	32	uneq2i	⊢ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) = ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } )
34	33	mpteq2i	⊢ ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) )
35	7	rabeqi	⊢ { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = { 𝑎 ∈ ∅ ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) }
36		rab0	⊢ { 𝑎 ∈ ∅ ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = ∅
37	35 36	eqtri	⊢ { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } = ∅
38	37	eqeq2i	⊢ ( 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ↔ 𝑦 = ∅ )
39	38	anbi2i	⊢ ( ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = ∅ ) )
40	39	2rexbii	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = ∅ ) )
41		r19.41vv	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = ∅ ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = ∅ ) )
42	40 41	bitri	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = ∅ ) )
43	42	biancomi	⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) ↔ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) )
44	43	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) }
45		rdgeq12	⊢ ( ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) = ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) → rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) = rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) )
46	34 44 45	mp2an	⊢ rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) = rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } )
47	46	reseq1i	⊢ ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( ∅ ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ∀ 𝑧 ∈ ∅ ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( ∅ ↑_m ω ) ∣ ( 𝑎 ‘ 𝑖 ) ∅ ( 𝑎 ‘ 𝑗 ) } ) } ) ↾ suc ω ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ↾ suc ω )
48	3 47	eqtri	⊢ ( ∅ Sat ∅ ) = ( rec ( ( 𝑓 ∈ V ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢 ∈ 𝑓 ( ∃ 𝑣 ∈ 𝑓 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖 ∈_𝑔 𝑗 ) ) } ) ↾ suc ω )

Metamath Proof Explorer

Theorem satf0

Proof