Theorem satf0op 32624

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 6670	. . . 4 ⊢ (𝑦 = ∅ → (𝑆‘𝑦) = (𝑆‘∅))
2	1	eleq2d 2898	. . 3 ⊢ (𝑦 = ∅ → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘∅)))
3	1	eleq2d 2898	. . . . 5 ⊢ (𝑦 = ∅ → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
4	3	anbi2d 630	. . . 4 ⊢ (𝑦 = ∅ → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
5	4	exbidv 1922	. . 3 ⊢ (𝑦 = ∅ → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
6	2, 5	bibi12d 348	. 2 ⊢ (𝑦 = ∅ → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))))
7		fveq2 6670	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑆‘𝑦) = (𝑆‘𝑧))
8	7	eleq2d 2898	. . 3 ⊢ (𝑦 = 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑧)))
9	7	eleq2d 2898	. . . . 5 ⊢ (𝑦 = 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))
10	9	anbi2d 630	. . . 4 ⊢ (𝑦 = 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))))
11	10	exbidv 1922	. . 3 ⊢ (𝑦 = 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))))
12	8, 11	bibi12d 348	. 2 ⊢ (𝑦 = 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))))
13		fveq2 6670	. . . 4 ⊢ (𝑦 = suc 𝑧 → (𝑆‘𝑦) = (𝑆‘suc 𝑧))
14	13	eleq2d 2898	. . 3 ⊢ (𝑦 = suc 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘suc 𝑧)))
15	13	eleq2d 2898	. . . . 5 ⊢ (𝑦 = suc 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))
16	15	anbi2d 630	. . . 4 ⊢ (𝑦 = suc 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
17	16	exbidv 1922	. . 3 ⊢ (𝑦 = suc 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
18	14, 17	bibi12d 348	. 2 ⊢ (𝑦 = suc 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))))
19		fveq2 6670	. . . 4 ⊢ (𝑦 = 𝑁 → (𝑆‘𝑦) = (𝑆‘𝑁))
20	19	eleq2d 2898	. . 3 ⊢ (𝑦 = 𝑁 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑁)))
21	19	eleq2d 2898	. . . . 5 ⊢ (𝑦 = 𝑁 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁)))
22	21	anbi2d 630	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))
23	22	exbidv 1922	. . 3 ⊢ (𝑦 = 𝑁 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))
24	20, 23	bibi12d 348	. 2 ⊢ (𝑦 = 𝑁 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁)))))
25		satf0op.s	. . . . . 6 ⊢ 𝑆 = (∅ Sat ∅)
26	25	fveq1i 6671	. . . . 5 ⊢ (𝑆‘∅) = ((∅ Sat ∅)‘∅)
27		satf00 32621	. . . . 5 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
28	26, 27	eqtri 2844	. . . 4 ⊢ (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
29	28	eleq2i 2904	. . 3 ⊢ (𝑋 ∈ (𝑆‘∅) ↔ 𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})
30		elopab 5414	. . 3 ⊢ (𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ ∃𝑥∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
31		opeq2 4804	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
32	31	adantr 483	. . . . . . . . . 10 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
33	32	eqeq2d 2832	. . . . . . . . 9 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
34	33	biimpd 231	. . . . . . . 8 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ → 𝑋 = ⟨𝑥, ∅⟩))
35	34	impcom 410	. . . . . . 7 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 𝑋 = ⟨𝑥, ∅⟩)
36		eqidd 2822	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → ∅ = ∅)
37	36	anim1i 616	. . . . . . . . 9 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
38	37	adantl 484	. . . . . . . 8 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
39		satf00 32621	. . . . . . . . . . 11 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}
40	26, 39	eqtri 2844	. . . . . . . . . 10 ⊢ (𝑆‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}
41	40	eleq2i 2904	. . . . . . . . 9 ⊢ (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ ⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))})
42		vex 3497	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
43		0ex 5211	. . . . . . . . . 10 ⊢ ∅ ∈ V
44		eqeq1 2825	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ = ∅))
45		eqeq1 2825	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑖∈𝑔𝑗)))
46	45	2rexbidv 3300	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
47	44, 46	bi2anan9r 638	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑥 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
48	42, 43, 47	opelopaba 5423	. . . . . . . . 9 ⊢ (⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
49	41, 48	bitri 277	. . . . . . . 8 ⊢ (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
50	38, 49	sylibr 236	. . . . . . 7 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))
51	35, 50	jca 514	. . . . . 6 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
52	51	exlimiv 1931	. . . . 5 ⊢ (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
53	31	eqeq2d 2832	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
54		eqeq1 2825	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ = ∅))
55	54	anbi1d 631	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
56	53, 55	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))))
57	43, 56	spcev 3607	. . . . . 6 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
58	49, 57	sylan2b 595	. . . . 5 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
59	52, 58	impbii 211	. . . 4 ⊢ (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
60	59	exbii 1848	. . 3 ⊢ (∃𝑥∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
61	29, 30, 60	3bitri 299	. 2 ⊢ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
62	25	satf0suc 32623	. . . . . . 7 ⊢ (𝑧 ∈ ω → (𝑆‘suc 𝑧) = ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
63	62	eleq2d 2898	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ 𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
64		elun 4125	. . . . . . 7 ⊢ (𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
65	64	a1i 11	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
66		elopab 5414	. . . . . . . 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 307	. . . . 5 ⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))))
70	69	adantr 483	. . . 4 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))))
71		simpr 487	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))))
72		opeq2 4804	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ∅ → ⟨𝑎, 𝑏⟩ = ⟨𝑎, ∅⟩)
73	72	eqeq2d 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
74	73	biimpd 231	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
75	74	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
76	75	impcom 410	. . . . . . . . . . . . 13 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → 𝑋 = ⟨𝑎, ∅⟩)
77		eqidd 2822	. . . . . . . . . . . . . 14 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → ∅ = ∅)
78		simpr 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
79	78	adantl 484	. . . . . . . . . . . . . 14 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
80	77, 79	jca 514	. . . . . . . . . . . . 13 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))
81	76, 80	jca 514	. . . . . . . . . . . 12 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
82	81	exlimiv 1931	. . . . . . . . . . 11 ⊢ (∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
83		eqeq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑏 = ∅ → (𝑏 = ∅ ↔ ∅ = ∅))
84	83	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (𝑏 = ∅ → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
85	73, 84	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑏 = ∅ → ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))))
86	43, 85	spcev 3607	. . . . . . . . . . 11 ⊢ ((𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
87	82, 86	impbii 211	. . . . . . . . . 10 ⊢ (∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
88	87	exbii 1848	. . . . . . . . 9 ⊢ (∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
89	88	a1i 11	. . . . . . . 8 ⊢ (𝑧 ∈ ω → (∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))))
90		opeq1 4803	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → ⟨𝑥, ∅⟩ = ⟨𝑎, ∅⟩)
91	90	eqeq2d 2832	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑋 = ⟨𝑥, ∅⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
92		eqeq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ 𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
93	92	rexbidv 3297	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
94		eqeq1 2825	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
95	94	rexbidv 3297	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
96	93, 95	orbi12d 915	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))
97	96	rexbidv 3297	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))
98	97	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → ((∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
99	91, 98	anbi12d 632	. . . . . . . . 9 ⊢ (𝑥 = 𝑎 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))))
100	99	cbvexvw 2044	. . . . . . . 8 ⊢ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑎(𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
101	89, 100	syl6bbr 291	. . . . . . 7 ⊢ (𝑧 ∈ ω → (∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
102	101	adantr 483	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → (∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
103	71, 102	orbi12d 915	. . . . 5 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
104		19.43 1883	. . . . . 6 ⊢ (∃𝑥((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
105		andi 1004	. . . . . . . 8 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
106	105	bicomi 226	. . . . . . 7 ⊢ (((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
107	106	exbii 1848	. . . . . 6 ⊢ (∃𝑥((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
108	104, 107	bitr3i 279	. . . . 5 ⊢ ((∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
109	103, 108	syl6bb 289	. . . 4 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
110	62	eleq2d 2898	. . . . . . . . 9 ⊢ (𝑧 ∈ ω → (⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧) ↔ ⟨𝑥, ∅⟩ ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
111		elun 4125	. . . . . . . . . 10 ⊢ (⟨𝑥, ∅⟩ ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ ⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
112		eqeq1 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
113	112	rexbidv 3297	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
114		eqeq1 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))
115	114	rexbidv 3297	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))
116	113, 115	orbi12d 915	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
117	116	rexbidv 3297	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑥 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
118	83, 117	bi2anan9r 638	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = ∅) → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))
119	42, 43, 118	opelopaba 5423	. . . . . . . . . . 11 ⊢ (⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
120	119	orbi2i 909	. . . . . . . . . 10 ⊢ ((⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ ⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))
121	111, 120	bitri 277	. . . . . . . . 9 ⊢ (⟨𝑥, ∅⟩ ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))
122	110, 121	syl6bb 289	. . . . . . . 8 ⊢ (𝑧 ∈ ω → (⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
123	122	anbi2d 630	. . . . . . 7 ⊢ (𝑧 ∈ ω → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
124	123	exbidv 1922	. . . . . 6 ⊢ (𝑧 ∈ ω → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
125	124	bicomd 225	. . . . 5 ⊢ (𝑧 ∈ ω → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
126	125	adantr 483	. . . 4 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
127	70, 109, 126	3bitrd 307	. . 3 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
128	127	ex 415	. 2 ⊢ (𝑧 ∈ ω → ((𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))) → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))))
129	6, 12, 18, 24, 61, 128	finds 7608	1 ⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139   ∪ cun 3934  ∅c0 4291  ⟨cop 4573  {copab 5128  suc csuc 6193  ‘cfv 6355  (class class class)co 7156  ωcom 7580  1^st c1st 7687  ∈_𝑔cgoe 32580  ⊼_𝑔cgna 32581  ∀_𝑔cgol 32582   Sat csat 32583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-inf2 9104

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-map 8408  df-goel 32587  df-sat 32590

This theorem is referenced by:  fmlasuc  32633