Metamath Proof Explorer


Theorem satf0op

Description: An element of a value of the satisfaction predicate as function over wff codes in the empty model and the empty binary relation expressed as ordered pair. (Contributed by AV, 19-Sep-2023)

Ref Expression
Hypothesis satf0op.s 𝑆 = ( ∅ Sat ∅ )
Assertion satf0op ( 𝑁 ∈ ω → ( 𝑋 ∈ ( 𝑆𝑁 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 satf0op.s 𝑆 = ( ∅ Sat ∅ )
2 fveq2 ( 𝑦 = ∅ → ( 𝑆𝑦 ) = ( 𝑆 ‘ ∅ ) )
3 2 eleq2d ( 𝑦 = ∅ → ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ 𝑋 ∈ ( 𝑆 ‘ ∅ ) ) )
4 2 eleq2d ( 𝑦 = ∅ → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
5 4 anbi2d ( 𝑦 = ∅ → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) ) )
6 5 exbidv ( 𝑦 = ∅ → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) ) )
7 3 6 bibi12d ( 𝑦 = ∅ → ( ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ) ↔ ( 𝑋 ∈ ( 𝑆 ‘ ∅ ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) ) ) )
8 fveq2 ( 𝑦 = 𝑧 → ( 𝑆𝑦 ) = ( 𝑆𝑧 ) )
9 8 eleq2d ( 𝑦 = 𝑧 → ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ 𝑋 ∈ ( 𝑆𝑧 ) ) )
10 8 eleq2d ( 𝑦 = 𝑧 → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) )
11 10 anbi2d ( 𝑦 = 𝑧 → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) )
12 11 exbidv ( 𝑦 = 𝑧 → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) )
13 9 12 bibi12d ( 𝑦 = 𝑧 → ( ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) )
14 fveq2 ( 𝑦 = suc 𝑧 → ( 𝑆𝑦 ) = ( 𝑆 ‘ suc 𝑧 ) )
15 14 eleq2d ( 𝑦 = suc 𝑧 → ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ) )
16 14 eleq2d ( 𝑦 = suc 𝑧 → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) )
17 16 anbi2d ( 𝑦 = suc 𝑧 → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) )
18 17 exbidv ( 𝑦 = suc 𝑧 → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) )
19 15 18 bibi12d ( 𝑦 = suc 𝑧 → ( ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ) ↔ ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) ) )
20 fveq2 ( 𝑦 = 𝑁 → ( 𝑆𝑦 ) = ( 𝑆𝑁 ) )
21 20 eleq2d ( 𝑦 = 𝑁 → ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ 𝑋 ∈ ( 𝑆𝑁 ) ) )
22 20 eleq2d ( 𝑦 = 𝑁 → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) )
23 22 anbi2d ( 𝑦 = 𝑁 → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) ) )
24 23 exbidv ( 𝑦 = 𝑁 → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) ) )
25 21 24 bibi12d ( 𝑦 = 𝑁 → ( ( 𝑋 ∈ ( 𝑆𝑦 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑦 ) ) ) ↔ ( 𝑋 ∈ ( 𝑆𝑁 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) ) ) )
26 1 fveq1i ( 𝑆 ‘ ∅ ) = ( ( ∅ Sat ∅ ) ‘ ∅ )
27 satf00 ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) }
28 26 27 eqtri ( 𝑆 ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) }
29 28 eleq2i ( 𝑋 ∈ ( 𝑆 ‘ ∅ ) ↔ 𝑋 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } )
30 elopab ( 𝑋 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) } ↔ ∃ 𝑥𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) )
31 opeq2 ( 𝑦 = ∅ → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ∅ ⟩ )
32 31 adantr ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ∅ ⟩ )
33 32 eqeq2d ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , ∅ ⟩ ) )
34 33 biimpd ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑋 = ⟨ 𝑥 , ∅ ⟩ ) )
35 34 impcom ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → 𝑋 = ⟨ 𝑥 , ∅ ⟩ )
36 eqidd ( 𝑦 = ∅ → ∅ = ∅ )
37 36 anim1i ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) → ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
38 37 adantl ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
39 satf00 ( ( ∅ Sat ∅ ) ‘ ∅ ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ) }
40 26 39 eqtri ( 𝑆 ‘ ∅ ) = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ) }
41 40 eleq2i ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ) } )
42 vex 𝑥 ∈ V
43 0ex ∅ ∈ V
44 eqeq1 ( 𝑧 = ∅ → ( 𝑧 = ∅ ↔ ∅ = ∅ ) )
45 eqeq1 ( 𝑦 = 𝑥 → ( 𝑦 = ( 𝑖𝑔 𝑗 ) ↔ 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
46 45 2rexbidv ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
47 44 46 bi2anan9r ( ( 𝑦 = 𝑥𝑧 = ∅ ) → ( ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) )
48 42 43 47 opelopaba ( ⟨ 𝑥 , ∅ ⟩ ∈ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( 𝑧 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑦 = ( 𝑖𝑔 𝑗 ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
49 41 48 bitri ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) )
50 38 49 sylibr ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) )
51 35 50 jca ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
52 51 exlimiv ( ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
53 31 eqeq2d ( 𝑦 = ∅ → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 𝑥 , ∅ ⟩ ) )
54 eqeq1 ( 𝑦 = ∅ → ( 𝑦 = ∅ ↔ ∅ = ∅ ) )
55 54 anbi1d ( 𝑦 = ∅ → ( ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) )
56 53 55 anbi12d ( 𝑦 = ∅ → ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) ) )
57 43 56 spcev ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) → ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) )
58 49 57 sylan2b ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) → ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) )
59 52 58 impbii ( ∃ 𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
60 59 exbii ( ∃ 𝑥𝑦 ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑦 = ∅ ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω 𝑥 = ( 𝑖𝑔 𝑗 ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
61 29 30 60 3bitri ( 𝑋 ∈ ( 𝑆 ‘ ∅ ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ ∅ ) ) )
62 1 satf0suc ( 𝑧 ∈ ω → ( 𝑆 ‘ suc 𝑧 ) = ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) )
63 62 eleq2d ( 𝑧 ∈ ω → ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ 𝑋 ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ) )
64 elun ( 𝑋 ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ 𝑋 ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) )
65 64 a1i ( 𝑧 ∈ ω → ( 𝑋 ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ 𝑋 ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ) )
66 elopab ( 𝑋 ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ↔ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
67 66 a1i ( 𝑧 ∈ ω → ( 𝑋 ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ↔ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
68 67 orbi2d ( 𝑧 ∈ ω → ( ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ 𝑋 ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
69 63 65 68 3bitrd ( 𝑧 ∈ ω → ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
70 69 adantr ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
71 simpr ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) )
72 opeq2 ( 𝑏 = ∅ → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , ∅ ⟩ )
73 72 eqeq2d ( 𝑏 = ∅ → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑋 = ⟨ 𝑎 , ∅ ⟩ ) )
74 73 biimpd ( 𝑏 = ∅ → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → 𝑋 = ⟨ 𝑎 , ∅ ⟩ ) )
75 74 adantr ( ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) → ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ → 𝑋 = ⟨ 𝑎 , ∅ ⟩ ) )
76 75 impcom ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → 𝑋 = ⟨ 𝑎 , ∅ ⟩ )
77 eqidd ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ∅ = ∅ )
78 simpr ( ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) → ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
79 78 adantl ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
80 77 79 jca ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
81 76 80 jca ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
82 81 exlimiv ( ∃ 𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
83 eqeq1 ( 𝑏 = ∅ → ( 𝑏 = ∅ ↔ ∅ = ∅ ) )
84 83 anbi1d ( 𝑏 = ∅ → ( ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
85 73 84 anbi12d ( 𝑏 = ∅ → ( ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
86 43 85 spcev ( ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) → ∃ 𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
87 82 86 impbii ( ∃ 𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
88 87 exbii ( ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ∃ 𝑎 ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
89 88 a1i ( 𝑧 ∈ ω → ( ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ∃ 𝑎 ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
90 opeq1 ( 𝑥 = 𝑎 → ⟨ 𝑥 , ∅ ⟩ = ⟨ 𝑎 , ∅ ⟩ )
91 90 eqeq2d ( 𝑥 = 𝑎 → ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ↔ 𝑋 = ⟨ 𝑎 , ∅ ⟩ ) )
92 eqeq1 ( 𝑥 = 𝑎 → ( 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ↔ 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ) )
93 92 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ↔ ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ) )
94 eqeq1 ( 𝑥 = 𝑎 → ( 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ↔ 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
95 94 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ↔ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
96 93 95 orbi12d ( 𝑥 = 𝑎 → ( ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
97 96 rexbidv ( 𝑥 = 𝑎 → ( ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
98 97 anbi2d ( 𝑥 = 𝑎 → ( ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
99 91 98 anbi12d ( 𝑥 = 𝑎 → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
100 99 cbvexvw ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ∃ 𝑎 ( 𝑋 = ⟨ 𝑎 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
101 89 100 bitr4di ( 𝑧 ∈ ω → ( ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
102 101 adantr ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
103 71 102 orbi12d ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
104 19.43 ( ∃ 𝑥 ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
105 andi ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
106 105 bicomi ( ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
107 106 exbii ( ∃ 𝑥 ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
108 104 107 bitr3i ( ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ∨ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
109 103 108 bitrdi ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( ( 𝑋 ∈ ( 𝑆𝑧 ) ∨ ∃ 𝑎𝑏 ( 𝑋 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
110 62 eleq2d ( 𝑧 ∈ ω → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ) )
111 elun ( ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) )
112 eqeq1 ( 𝑎 = 𝑥 → ( 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ↔ 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ) )
113 112 rexbidv ( 𝑎 = 𝑥 → ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ↔ ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ) )
114 eqeq1 ( 𝑎 = 𝑥 → ( 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ↔ 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
115 114 rexbidv ( 𝑎 = 𝑥 → ( ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ↔ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) )
116 113 115 orbi12d ( 𝑎 = 𝑥 → ( ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ↔ ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
117 116 rexbidv ( 𝑎 = 𝑥 → ( ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ↔ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
118 83 117 bi2anan9r ( ( 𝑎 = 𝑥𝑏 = ∅ ) → ( ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
119 42 43 118 opelopaba ( ⟨ 𝑥 , ∅ ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ↔ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) )
120 119 orbi2i ( ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ⟨ 𝑥 , ∅ ⟩ ∈ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
121 111 120 bitri ( ⟨ 𝑥 , ∅ ⟩ ∈ ( ( 𝑆𝑧 ) ∪ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑏 = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑎 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑎 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) } ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) )
122 110 121 bitrdi ( 𝑧 ∈ ω → ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) )
123 122 anbi2d ( 𝑧 ∈ ω → ( ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ↔ ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
124 123 exbidv ( 𝑧 ∈ ω → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ) )
125 124 bicomd ( 𝑧 ∈ ω → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) )
126 125 adantr ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ( ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ∨ ( ∅ = ∅ ∧ ∃ 𝑢 ∈ ( 𝑆𝑧 ) ( ∃ 𝑣 ∈ ( 𝑆𝑧 ) 𝑥 = ( ( 1st𝑢 ) ⊼𝑔 ( 1st𝑣 ) ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 ( 1st𝑢 ) ) ) ) ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) )
127 70 109 126 3bitrd ( ( 𝑧 ∈ ω ∧ ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) ) → ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) )
128 127 ex ( 𝑧 ∈ ω → ( ( 𝑋 ∈ ( 𝑆𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑧 ) ) ) → ( 𝑋 ∈ ( 𝑆 ‘ suc 𝑧 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ suc 𝑧 ) ) ) ) )
129 7 13 19 25 61 128 finds ( 𝑁 ∈ ω → ( 𝑋 ∈ ( 𝑆𝑁 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆𝑁 ) ) ) )