Theorem satf0op 34895

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.)

Hypothesis

Ref	Expression
satf0op.s	⊢ 𝑆 = (∅ Sat ∅)

Assertion

Ref	Expression
satf0op	⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))

Distinct variable groups:   𝑥,𝑁   𝑥,𝑆   𝑥,𝑋

Proof of Theorem satf0op

Dummy variables 𝑖 𝑗 𝑦 𝑧 𝑎 𝑏 𝑢 𝑣 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∃wrex 3064   ∪ cun 3941  ∅c0 4317  ⟨cop 4629  {copab 5203  suc csuc 6359  ‘cfv 6536  (class class class)co 7404  ωcom 7851  1^st c1st 7969  ∈_𝑔cgoe 34851  ⊼_𝑔cgna 34852  ∀_𝑔cgol 34853   Sat csat 34854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-inf2 9635

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-map 8821  df-goel 34858  df-sat 34861

This theorem is referenced by:  fmlasuc  34904