Metamath Proof Explorer


Theorem 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 ↦ ( 𝑓 ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑢𝑓 ( ∃ 𝑣𝑓 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ) , { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } ) ↾ suc ω )

Proof

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