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

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 ⊢ ( 𝑁 ∈ ω → ( 𝑋 ∈ ( 𝑆 ‘ 𝑁 ) ↔ ∃ 𝑥 ( 𝑋 = ⟨ 𝑥 , ∅ ⟩ ∧ ⟨ 𝑥 , ∅ ⟩ ∈ ( 𝑆 ‘ 𝑁 ) ) ) )