Theorem satf0op 35382

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 6906	. . . 4 ⊢ (𝑦 = ∅ → (𝑆‘𝑦) = (𝑆‘∅))
2	1	eleq2d 2827	. . 3 ⊢ (𝑦 = ∅ → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘∅)))
3	1	eleq2d 2827	. . . . 5 ⊢ (𝑦 = ∅ → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
4	3	anbi2d 630	. . . 4 ⊢ (𝑦 = ∅ → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
5	4	exbidv 1921	. . 3 ⊢ (𝑦 = ∅ → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))))
6	2, 5	bibi12d 345	. 2 ⊢ (𝑦 = ∅ → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))))
7		fveq2 6906	. . . 4 ⊢ (𝑦 = 𝑧 → (𝑆‘𝑦) = (𝑆‘𝑧))
8	7	eleq2d 2827	. . 3 ⊢ (𝑦 = 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑧)))
9	7	eleq2d 2827	. . . . 5 ⊢ (𝑦 = 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))
10	9	anbi2d 630	. . . 4 ⊢ (𝑦 = 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))))
11	10	exbidv 1921	. . 3 ⊢ (𝑦 = 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧))))
12	8, 11	bibi12d 345	. 2 ⊢ (𝑦 = 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))))
13		fveq2 6906	. . . 4 ⊢ (𝑦 = suc 𝑧 → (𝑆‘𝑦) = (𝑆‘suc 𝑧))
14	13	eleq2d 2827	. . 3 ⊢ (𝑦 = suc 𝑧 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘suc 𝑧)))
15	13	eleq2d 2827	. . . . 5 ⊢ (𝑦 = suc 𝑧 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))
16	15	anbi2d 630	. . . 4 ⊢ (𝑦 = suc 𝑧 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
17	16	exbidv 1921	. . 3 ⊢ (𝑦 = suc 𝑧 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧))))
18	14, 17	bibi12d 345	. 2 ⊢ (𝑦 = suc 𝑧 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘suc 𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)))))
19		fveq2 6906	. . . 4 ⊢ (𝑦 = 𝑁 → (𝑆‘𝑦) = (𝑆‘𝑁))
20	19	eleq2d 2827	. . 3 ⊢ (𝑦 = 𝑁 → (𝑋 ∈ (𝑆‘𝑦) ↔ 𝑋 ∈ (𝑆‘𝑁)))
21	19	eleq2d 2827	. . . . 5 ⊢ (𝑦 = 𝑁 → (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦) ↔ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁)))
22	21	anbi2d 630	. . . 4 ⊢ (𝑦 = 𝑁 → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))
23	22	exbidv 1921	. . 3 ⊢ (𝑦 = 𝑁 → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))
24	20, 23	bibi12d 345	. 2 ⊢ (𝑦 = 𝑁 → ((𝑋 ∈ (𝑆‘𝑦) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑦))) ↔ (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁)))))
25		satf0op.s	. . . . . 6 ⊢ 𝑆 = (∅ Sat ∅)
26	25	fveq1i 6907	. . . . 5 ⊢ (𝑆‘∅) = ((∅ Sat ∅)‘∅)
27		satf00 35379	. . . . 5 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
28	26, 27	eqtri 2765	. . . 4 ⊢ (𝑆‘∅) = {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))}
29	28	eleq2i 2833	. . 3 ⊢ (𝑋 ∈ (𝑆‘∅) ↔ 𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))})
30		elopab 5532	. . 3 ⊢ (𝑋 ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))} ↔ ∃𝑥∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
31		opeq2 4874	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
32	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∅⟩)
33	32	eqeq2d 2748	. . . . . . . . 9 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
34	33	biimpd 229	. . . . . . . 8 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (𝑋 = ⟨𝑥, 𝑦⟩ → 𝑋 = ⟨𝑥, ∅⟩))
35	34	impcom 407	. . . . . . 7 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → 𝑋 = ⟨𝑥, ∅⟩)
36		eqidd 2738	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → ∅ = ∅)
37	36	anim1i 615	. . . . . . . . 9 ⊢ ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
38	37	adantl 481	. . . . . . . 8 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
39		satf00 35379	. . . . . . . . . . 11 ⊢ ((∅ Sat ∅)‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}
40	26, 39	eqtri 2765	. . . . . . . . . 10 ⊢ (𝑆‘∅) = {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))}
41	40	eleq2i 2833	. . . . . . . . 9 ⊢ (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ ⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))})
42		vex 3484	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
43		0ex 5307	. . . . . . . . . 10 ⊢ ∅ ∈ V
44		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑧 = ∅ → (𝑧 = ∅ ↔ ∅ = ∅))
45		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑥 → (𝑦 = (𝑖∈𝑔𝑗) ↔ 𝑥 = (𝑖∈𝑔𝑗)))
46	45	2rexbidv 3222	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑥 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
47	44, 46	bi2anan9r 639	. . . . . . . . . 10 ⊢ ((𝑦 = 𝑥 ∧ 𝑧 = ∅) → ((𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
48	42, 43, 47	opelopaba 5541	. . . . . . . . 9 ⊢ (⟨𝑥, ∅⟩ ∈ {⟨𝑦, 𝑧⟩ ∣ (𝑧 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑦 = (𝑖∈𝑔𝑗))} ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
49	41, 48	bitri 275	. . . . . . . 8 ⊢ (⟨𝑥, ∅⟩ ∈ (𝑆‘∅) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))
50	38, 49	sylibr 234	. . . . . . 7 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → ⟨𝑥, ∅⟩ ∈ (𝑆‘∅))
51	35, 50	jca 511	. . . . . 6 ⊢ ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
52	51	exlimiv 1930	. . . . 5 ⊢ (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
53	31	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑋 = ⟨𝑥, 𝑦⟩ ↔ 𝑋 = ⟨𝑥, ∅⟩))
54		eqeq1 2741	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑦 = ∅ ↔ ∅ = ∅))
55	54	anbi1d 631	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)) ↔ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
56	53, 55	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗)))))
57	43, 56	spcev 3606	. . . . . 6 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
58	49, 57	sylan2b 594	. . . . 5 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)) → ∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))))
59	52, 58	impbii 209	. . . 4 ⊢ (∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
60	59	exbii 1848	. . 3 ⊢ (∃𝑥∃𝑦(𝑋 = ⟨𝑥, 𝑦⟩ ∧ (𝑦 = ∅ ∧ ∃𝑖 ∈ ω ∃𝑗 ∈ ω 𝑥 = (𝑖∈𝑔𝑗))) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
61	29, 30, 60	3bitri 297	. 2 ⊢ (𝑋 ∈ (𝑆‘∅) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘∅)))
62	25	satf0suc 35381	. . . . . . 7 ⊢ (𝑧 ∈ ω → (𝑆‘suc 𝑧) = ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
63	62	eleq2d 2827	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝑋 ∈ (𝑆‘suc 𝑧) ↔ 𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
64		elun 4153	. . . . . . 7 ⊢ (𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
65	64	a1i 11	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝑋 ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (𝑋 ∈ (𝑆‘𝑧) ∨ 𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
66		elopab 5532	. . . . . . . 8 ⊢ (𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
67	66	a1i 11	. . . . . . 7 ⊢ (𝑧 ∈ ω → (𝑋 ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))} ↔ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))))
68	67	orbi2d 916	. . . . . 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 4874	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = ∅ → ⟨𝑎, 𝑏⟩ = ⟨𝑎, ∅⟩)
73	72	eqeq2d 2748	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
74	73	biimpd 229	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = ∅ → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
75	74	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) → (𝑋 = ⟨𝑎, 𝑏⟩ → 𝑋 = ⟨𝑎, ∅⟩))
76	75	impcom 407	. . . . . . . . . . . . 13 ⊢ ((𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → 𝑋 = ⟨𝑎, ∅⟩)
77		eqidd 2738	. . . . . . . . . . . . . 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 1930	. . . . . . . . . . 11 ⊢ (∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → (𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
83		eqeq1 2741	. . . . . . . . . . . . . 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 3606	. . . . . . . . . . 11 ⊢ ((𝑋 = ⟨𝑎, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))) → ∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))))
87	82, 86	impbii 209	. . . . . . . . . 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 4873	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑎 → ⟨𝑥, ∅⟩ = ⟨𝑎, ∅⟩)
91	90	eqeq2d 2748	. . . . . . . . . 10 ⊢ (𝑥 = 𝑎 → (𝑋 = ⟨𝑥, ∅⟩ ↔ 𝑋 = ⟨𝑎, ∅⟩))
92		eqeq1 2741	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ 𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
93	92	rexbidv 3179	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
94		eqeq1 2741	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
95	94	rexbidv 3179	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))
96	93, 95	orbi12d 919	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))
97	96	rexbidv 3179	. . . . . . . . . . 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 2036	. . . . . . . 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 919	. . . . 5 ⊢ ((𝑧 ∈ ω ∧ (𝑋 ∈ (𝑆‘𝑧) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)))) → ((𝑋 ∈ (𝑆‘𝑧) ∨ ∃𝑎∃𝑏(𝑋 = ⟨𝑎, 𝑏⟩ ∧ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
104		19.43 1882	. . . . . 6 ⊢ (∃𝑥((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
105		andi 1010	. . . . . . . 8 ⊢ ((𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
106	105	bicomi 224	. . . . . . 7 ⊢ (((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧)) ∨ (𝑋 = ⟨𝑥, ∅⟩ ∧ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))))
107	106	exbii 1848	. . . . . 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 2827	. . . . . . . . 9 ⊢ (𝑧 ∈ ω → (⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧) ↔ ⟨𝑥, ∅⟩ ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))})))
111		elun 4153	. . . . . . . . . 10 ⊢ (⟨𝑥, ∅⟩ ∈ ((𝑆‘𝑧) ∪ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}) ↔ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ ⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))}))
112		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
113	112	rexbidv 3179	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ↔ ∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣))))
114		eqeq1 2741	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → (𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))
115	114	rexbidv 3179	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑥 → (∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))
116	113, 115	orbi12d 919	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑥 → ((∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
117	116	rexbidv 3179	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑥 → (∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)) ↔ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
118	83, 117	bi2anan9r 639	. . . . . . . . . . . 12 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = ∅) → ((𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢))) ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))
119	42, 43, 118	opelopaba 5541	. . . . . . . . . . 11 ⊢ (⟨𝑥, ∅⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ (𝑏 = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑎 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑎 = ∀𝑔𝑖(1st ‘𝑢)))} ↔ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))))
120	119	orbi2i 913	. . . . . . . . . 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 630	. . . . . . 7 ⊢ (𝑧 ∈ ω → ((𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ (𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
124	123	exbidv 1921	. . . . . 6 ⊢ (𝑧 ∈ ω → (∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘suc 𝑧)) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ (⟨𝑥, ∅⟩ ∈ (𝑆‘𝑧) ∨ (∅ = ∅ ∧ ∃𝑢 ∈ (𝑆‘𝑧)(∃𝑣 ∈ (𝑆‘𝑧)𝑥 = ((1st ‘𝑢)⊼𝑔(1st ‘𝑣)) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))))))
125	124	bicomd 223	. . . . 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 7918	1 ⊢ (𝑁 ∈ ω → (𝑋 ∈ (𝑆‘𝑁) ↔ ∃𝑥(𝑋 = ⟨𝑥, ∅⟩ ∧ ⟨𝑥, ∅⟩ ∈ (𝑆‘𝑁))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070   ∪ cun 3949  ∅c0 4333  ⟨cop 4632  {copab 5205  suc csuc 6386  ‘cfv 6561  (class class class)co 7431  ωcom 7887  1^st c1st 8012  ∈_𝑔cgoe 35338  ⊼_𝑔cgna 35339  ∀_𝑔cgol 35340   Sat csat 35341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-map 8868  df-goel 35345  df-sat 35348

This theorem is referenced by:  fmlasuc  35391