Theorem cantnflem1 9681

Description: Lemma for cantnf 9685. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation 𝑇 is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct 𝐹, 𝐺 are 𝑇 -related as 𝐹 < 𝐺 or 𝐺 < 𝐹, and WLOG assuming that 𝐹 < 𝐺, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.)

Hypotheses

Ref	Expression
cantnfs.s	⊢ 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a	⊢ (𝜑 → 𝐴 ∈ On)
cantnfs.b	⊢ (𝜑 → 𝐵 ∈ On)
oemapval.t	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
oemapval.f	⊢ (𝜑 → 𝐹 ∈ 𝑆)
oemapval.g	⊢ (𝜑 → 𝐺 ∈ 𝑆)
oemapvali.r	⊢ (𝜑 → 𝐹𝑇𝐺)
oemapvali.x	⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}
cantnflem1.o	⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
cantnflem1.h	⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐺‘(𝑂‘𝑘))) +o 𝑧)), ∅)

Assertion

Ref	Expression
cantnflem1	⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Distinct variable groups:   𝑘,𝑐,𝑤,𝑥,𝑦,𝑧,𝐵   𝐴,𝑐,𝑘,𝑤,𝑥,𝑦,𝑧   𝑇,𝑐,𝑘   𝑘,𝐹,𝑤,𝑥,𝑦,𝑧   𝑆,𝑐,𝑘,𝑥,𝑦,𝑧   𝐺,𝑐,𝑘,𝑤,𝑥,𝑦,𝑧   𝑥,𝐻,𝑦   𝑘,𝑂,𝑤,𝑥,𝑦,𝑧   𝜑,𝑘,𝑥,𝑦,𝑧   𝑘,𝑋,𝑤,𝑥,𝑦,𝑧   𝐹,𝑐   𝜑,𝑐

Allowed substitution hints:   𝜑(𝑤)   𝑆(𝑤)   𝑇(𝑥,𝑦,𝑧,𝑤)   𝐻(𝑧,𝑤,𝑘,𝑐)   𝑂(𝑐)   𝑋(𝑐)

Proof of Theorem cantnflem1

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7439	. . . . . 6 ⊢ (𝐺 supp ∅) ∈ V
2		cantnflem1.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
3	2	oion 9528	. . . . . 6 ⊢ ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
4	1, 3	mp1i 13	. . . . 5 ⊢ (𝜑 → dom 𝑂 ∈ On)
5		uniexg 7727	. . . . 5 ⊢ (dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V)
6		sucidg 6443	. . . . 5 ⊢ (∪ dom 𝑂 ∈ V → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂)
7	4, 5, 6	3syl 18	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ suc ∪ dom 𝑂)
8		cantnfs.s	. . . . . . . . . 10 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
9		cantnfs.a	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ On)
10		cantnfs.b	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ On)
11		oemapval.t	. . . . . . . . . 10 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))}
12		oemapval.f	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
13		oemapval.g	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ∈ 𝑆)
14		oemapvali.r	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹𝑇𝐺)
15		oemapvali.x	. . . . . . . . . 10 ⊢ 𝑋 = ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}
16	8, 9, 10, 11, 12, 13, 14, 15	cantnflem1a 9677	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
17		n0i 4333	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19		ovexd 7441	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 supp ∅) ∈ V)
20	8, 9, 10, 2, 13	cantnfcl 9659	. . . . . . . . . . 11 ⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
21	20	simpld 496	. . . . . . . . . 10 ⊢ (𝜑 → E We (𝐺 supp ∅))
22	2	oien 9530	. . . . . . . . . 10 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
23	19, 21, 22	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24		breq1 5151	. . . . . . . . . 10 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25		ensymb 8995	. . . . . . . . . . 11 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26		en0 9010	. . . . . . . . . . 11 ⊢ ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
27	25, 26	bitri 275	. . . . . . . . . 10 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
28	24, 27	bitrdi 287	. . . . . . . . 9 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
29	23, 28	syl5ibcom 244	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
30	18, 29	mtod 197	. . . . . . 7 ⊢ (𝜑 → ¬ dom 𝑂 = ∅)
31	20	simprd 497	. . . . . . . 8 ⊢ (𝜑 → dom 𝑂 ∈ ω)
32		nnlim 7866	. . . . . . . 8 ⊢ (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
33	31, 32	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ Lim dom 𝑂)
34		ioran 983	. . . . . . 7 ⊢ (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
35	30, 33, 34	sylanbrc 584	. . . . . 6 ⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
36	2	oicl 9521	. . . . . . 7 ⊢ Ord dom 𝑂
37		unizlim 6485	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
38	36, 37	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
39	35, 38	mtbird 325	. . . . 5 ⊢ (𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂)
40		orduniorsuc 7815	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
41	36, 40	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
42	41	ord 863	. . . . 5 ⊢ (𝜑 → (¬ dom 𝑂 = ∪ dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂))
43	39, 42	mpd 15	. . . 4 ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂)
44	7, 43	eleqtrrd 2837	. . 3 ⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂)
45	2	oiiso 9529	. . . . . . . 8 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
46	19, 21, 45	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47		isof1o 7317	. . . . . . 7 ⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
48	46, 47	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
49		f1ocnv 6843	. . . . . 6 ⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50		f1of 6831	. . . . . 6 ⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
51	48, 49, 50	3syl 18	. . . . 5 ⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
52	51, 16	ffvelcdmd 7085	. . . 4 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂)
53		elssuni 4941	. . . 4 ⊢ ((◡𝑂‘𝑋) ∈ dom 𝑂 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . 3 ⊢ (𝜑 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
55	43, 31	eqeltrrd 2835	. . . . 5 ⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω)
56		peano2b 7869	. . . . 5 ⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω)
57	55, 56	sylibr 233	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ ω)
58		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂))
59		sseq2 4008	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂))
60	58, 59	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)))
61		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑂‘𝑦) = (𝑂‘∪ dom 𝑂))
62	61	sseq2d 4014	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
63	62	ifbid 4551	. . . . . . . . . 10 ⊢ (𝑦 = ∪ dom 𝑂 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
64	63	mpteq2dv 5250	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
65	64	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
66		suceq 6428	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂)
67	66	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc ∪ dom 𝑂))
68	65, 67	eleq12d 2828	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
69	60, 68	imbi12d 345	. . . . . 6 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
70	69	imbi2d 341	. . . . 5 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))))
71		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72		sseq2 4008	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∅))
73	71, 72	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅)))
74		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (𝑂‘𝑦) = (𝑂‘∅))
75	74	sseq2d 4014	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
76	75	ifbid 4551	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
77	76	mpteq2dv 5250	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
78	77	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
79		suceq 6428	. . . . . . . . 9 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
80	79	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
81	78, 80	eleq12d 2828	. . . . . . 7 ⊢ (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
82	73, 81	imbi12d 345	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂))
84		sseq2 4008	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ 𝑢))
85	83, 84	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)))
86		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑂‘𝑦) = (𝑂‘𝑢))
87	86	sseq2d 4014	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘𝑢)))
88	87	ifbid 4551	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
89	88	mpteq2dv 5250	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
90	89	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))
91		suceq 6428	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
92	91	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
93	90, 92	eleq12d 2828	. . . . . . 7 ⊢ (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
94	85, 93	imbi12d 345	. . . . . 6 ⊢ (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96		sseq2 4008	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ suc 𝑢))
97	95, 96	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢)))
98		fveq2 6889	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑢 → (𝑂‘𝑦) = (𝑂‘suc 𝑢))
99	98	sseq2d 4014	. . . . . . . . . . 11 ⊢ (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
100	99	ifbid 4551	. . . . . . . . . 10 ⊢ (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
101	100	mpteq2dv 5250	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
102	101	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
103		suceq 6428	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104	103	fveq2d 6893	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105	102, 104	eleq12d 2828	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
106	97, 105	imbi12d 345	. . . . . 6 ⊢ (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107		f1ocnvfv2 7272	. . . . . . . . . . . . 13 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
108	48, 16, 107	syl2anc 585	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
109	108	sseq2d 4014	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ 𝑋))
110	109	ifbid 4551	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))
111	110	mpteq2dv 5250	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)))
112	111	fveq2d 6893	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))))
113		cantnflem1.h	. . . . . . . . 9 ⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝑂‘𝑘)) ·o (𝐺‘(𝑂‘𝑘))) +o 𝑧)), ∅)
114	8, 9, 10, 11, 12, 13, 14, 15, 2, 113	cantnflem1d 9680	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
115	112, 114	eqeltrd 2834	. . . . . . 7 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
116		ss0 4398	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (◡𝑂‘𝑋) = ∅)
117	116	fveq2d 6893	. . . . . . . . . . . . 13 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘∅))
118	117	sseq2d 4014	. . . . . . . . . . . 12 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119	118	ifbid 4551	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
120	119	mpteq2dv 5250	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
121	120	fveq2d 6893	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
122		suceq 6428	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) = ∅ → suc (◡𝑂‘𝑋) = suc ∅)
123	116, 122	syl 17	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → suc (◡𝑂‘𝑋) = suc ∅)
124	123	fveq2d 6893	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc ∅))
125	121, 124	eleq12d 2828	. . . . . . . 8 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126	125	adantl 483	. . . . . . 7 ⊢ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127	115, 126	syl5ibcom 244	. . . . . 6 ⊢ (𝜑 → ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128		ordelon 6386	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On)
129	36, 52, 128	sylancr 588	. . . . . . . . . . 11 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On)
130	36	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord dom 𝑂)
131		ordelon 6386	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
132	130, 131	sylan 581	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133		onsseleq 6403	. . . . . . . . . . 11 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
134	129, 132, 133	syl2an2r 684	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
135		onsucb 7802	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
136	132, 135	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
137		eloni 6372	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ On → Ord 𝑢)
138	136, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
139		ordsssuc 6451	. . . . . . . . . . . . 13 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ Ord 𝑢) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
140	129, 138, 139	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
141		ordtr 6376	. . . . . . . . . . . . . . . . 17 ⊢ (Ord dom 𝑂 → Tr dom 𝑂)
142	36, 141	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
143		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
144		trsuc 6449	. . . . . . . . . . . . . . . 16 ⊢ ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
145	142, 143, 144	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
146		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ⊆ 𝑢)
147	145, 146	jca 513	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢))
148	10	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
149		oecl 8534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On)
150	9, 148, 149	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑o 𝐵) ∈ On)
151	9	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
152	8, 151, 148	cantnff 9666	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵))
153	8, 9, 10	cantnfs 9658	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
154	12, 153	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
155	154	simpld 496	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
156	155	ffvelcdmda 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) ∈ 𝐴)
157	8, 9, 10	cantnfs 9658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)))
158	13, 157	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))
159	158	simpld 496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
160	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 9676	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
161	160	simp1d 1143	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
162	159, 161	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
163	162	ne0d 4335	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ≠ ∅)
164		on0eln0 6418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
165	9, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
166	163, 165	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∅ ∈ 𝐴)
167	166	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∅ ∈ 𝐴)
168	156, 167	ifcld 4574	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ 𝐴)
169	168	fmpttd 7112	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴)
170	10	mptexd 7223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
171		funmpt 6584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
173	154	simprd 497	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 finSupp ∅)
174		ssidd 4005	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
175		0ex 5307	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ V
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∅ ∈ V)
177	155, 174, 10, 176	suppssr 8178	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑥) = ∅)
178	177	ifeq1d 4547	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
179		ifid 4568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅) = ∅
180	178, 179	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
181	180, 10	suppss2 8182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
182		fsuppsssupp 9376	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V ∧ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
183	170, 172, 173, 181, 182	syl22anc 838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
184	8, 9, 10	cantnfs 9658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)))
185	169, 183, 184	mpbir2and 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
186	185	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
187	152, 186	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑o 𝐵))
188		onelon 6387	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑o 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑o 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
189	150, 187, 188	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
190	31	adantr 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
191		elnn 7863	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
192	143, 190, 191	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
193	113	cantnfvalf 9657	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻:ω⟶On
194	193	ffvelcdmi 7083	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
195	192, 194	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
196		suppssdm 8159	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 supp ∅) ⊆ dom 𝐺
197	196, 159	fssdm 6735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
198	197	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
199	2	oif 9522	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅)
200	199	ffvelcdmi 7083	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
201	143, 200	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
202	198, 201	sseldd 3983	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
203		onelon 6387	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
204	10, 202, 203	syl2an2r 684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
205		oecl 8534	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴 ↑o (𝑂‘suc 𝑢)) ∈ On)
206	9, 204, 205	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑o (𝑂‘suc 𝑢)) ∈ On)
207	155	adantr 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐹:𝐵⟶𝐴)
208	207, 202	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
209		onelon 6387	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
210	9, 208, 209	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
211		omcl 8533	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑o (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
212	206, 210, 211	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
213		oaord 8544	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
214	189, 195, 212, 213	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
215		ifeq1 4532	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
216		ifid 4568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
217	215, 216	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = ∅)
218		ifeq1 4532	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅))
219		ifid 4568	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅) = ∅
220	218, 219	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = ∅)
221	217, 220	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) ↔ ∅ = ∅))
222		onss 7769	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
223	10, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ⊆ On)
224	223	sselda 3982	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
225	224	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
226	204	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
227		onsseleq 6403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
228	225, 226, 227	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
229	228	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
230	199	ffvelcdmi 7083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
231	145, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
232	198, 231	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵)
233		onelon 6387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On)
234	10, 232, 233	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On)
235	234	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑂‘𝑢) ∈ On)
236		onsssuc 6452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
237	225, 235, 236	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
238		vex 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑢 ∈ V
239	238	sucid 6444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ suc 𝑢
240	46	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
241		isorel 7320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
242	240, 145, 143, 241	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
243	238	sucex 7791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ suc 𝑢 ∈ V
244	243	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢)
245		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑂‘suc 𝑢) ∈ V
246	245	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
247	242, 244, 246	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢)))
248	239, 247	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
249		eloni 6372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
250	204, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
251		ordelsuc 7805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑂‘𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
252	234, 250, 251	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
253	248, 252	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
254	253	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
255	254	sseld 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
256	237, 255	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
257		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥)
258	240	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
259	258, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
260	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 9679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
261		f1ocnvfv2 7272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
262	259, 260, 261	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
263	257, 262	eleqtrrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
264	145	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
265	259, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
266	265, 260	ffvelcdmd 7085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
267		isorel 7320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
268	258, 264, 266, 267	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
269		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡𝑂‘𝑥) ∈ V
270	269	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 E (◡𝑂‘𝑥) ↔ 𝑢 ∈ (◡𝑂‘𝑥))
271		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑂‘(◡𝑂‘𝑥)) ∈ V
272	271	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
273	268, 270, 272	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥))))
274	263, 273	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ (◡𝑂‘𝑥))
275		ordelon 6386	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂) → (◡𝑂‘𝑥) ∈ On)
276	36, 266, 275	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ On)
277		eloni 6372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((◡𝑂‘𝑥) ∈ On → Ord (◡𝑂‘𝑥))
278	276, 277	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → Ord (◡𝑂‘𝑥))
279		ordelsuc 7805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ (◡𝑂‘𝑥) ∧ Ord (◡𝑂‘𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
280	274, 278, 279	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
281	274, 280	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (◡𝑂‘𝑥))
282	143	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
283	36, 282, 131	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
284		ontri1 6396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((suc 𝑢 ∈ On ∧ (◡𝑂‘𝑥) ∈ On) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
285	283, 276, 284	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
286	281, 285	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ (◡𝑂‘𝑥) ∈ suc 𝑢)
287		isorel 7320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
288	258, 266, 282, 287	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
289	243	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((◡𝑂‘𝑥) E suc 𝑢 ↔ (◡𝑂‘𝑥) ∈ suc 𝑢)
290	245	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢))
291	288, 289, 290	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢)))
292	262	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
293	291, 292	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
294	286, 293	mtbid 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
295	294	expr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑂‘𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
296	295	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂‘𝑢) ∈ 𝑥))
297		ontri1 6396	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
298	225, 235, 297	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
299	296, 298	sylibrd 259	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂‘𝑢)))
300	256, 299	impbid 211	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
301	300	orbi1d 916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
302	229, 301	bitr4d 282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
303		orcom 869	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)))
304	302, 303	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢))))
305	304	ifbid 4551	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
306		eqidd 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ∅ = ∅)
307	221, 305, 306	pm2.61ne 3028	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
308	307	mpteq2dva 5248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)))
309	308	fveq2d 6893	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))))
310		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑥) ∈ V
311	310, 175	ifex 4578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V
312	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
313	312	ralrimivw 3151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
314		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
315	314	fnmpt 6688	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
316	313, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
317	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∅ ∈ V)
318		suppvalfn 8151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅})
319		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝐵
320		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥𝐵
321		nffvmpt1 6900	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)
322		nfcv 2904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥∅
323	321, 322	nfne 3044	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅
324		nfv 1918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅
325		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥))
326	325	neeq1d 3001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅))
327	319, 320, 323, 324, 326	cbvrabw 3468	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅}
328	318, 327	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
329	316, 148, 317, 328	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
330		eqidd 2734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
331	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
332	330, 331	fvmpt2d 7009	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
333	332	neeq1d 3001	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
334	331	biantrurd 534	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)))
335		dif1o 8497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o) ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
336	334, 335	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)))
337	333, 336	bitrd 279	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)))
338	337	rabbidva 3440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)})
339	329, 338	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)})
340	311, 335	mpbiran 708	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o) ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)
341		ifeq1 4532	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
342	341, 179	eqtrdi 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
343	342	necon3i 2974	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → (𝐹‘𝑥) ≠ ∅)
344		iffalse 4537	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ⊆ (𝑂‘𝑢) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
345	344	necon1ai 2969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂‘𝑢))
346	343, 345	jca 513	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → ((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)))
347	256	expimpd 455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
348	346, 347	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
349	340, 348	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o) → 𝑥 ∈ (𝑂‘suc 𝑢)))
350	349	3impia 1118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵 ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)) → 𝑥 ∈ (𝑂‘suc 𝑢))
351	350	rabssdv 4072	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1o)} ⊆ (𝑂‘suc 𝑢))
352	339, 351	eqsstrd 4020	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
353		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
354		sseq1 4007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑦 ⊆ (𝑂‘𝑢)))
355	353, 354	orbi12d 918	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢))))
356		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
357	355, 356	ifbieq1d 4552	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
358	357	cbvmptv 5261	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
359		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑂‘suc 𝑢) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
360	359	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 = (𝑂‘suc 𝑢)) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
361	360	ifeq1da 4559	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
362	354, 356	ifbieq1d 4552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
363		fvex 6902	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑦) ∈ V
364	363, 175	ifex 4578	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅) ∈ V
365	362, 314, 364	fvmpt 6996	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
366	365	ifeq2d 4548	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅)))
367		ifor 4582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
368	366, 367	eqtr4di 2791	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
369	361, 368	eqtr3d 2775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
370	369	mpteq2ia 5251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
371	358, 370	eqtr4i 2764	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
372	8, 151, 148, 186, 202, 208, 352, 371	cantnfp1 9673	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))))
373	372	simprd 497	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
374	309, 373	eqtrd 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
375	8, 9, 10, 2, 13, 113	cantnfsuc 9662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
376	192, 375	syldan 592	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
377	160	simp3d 1145	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
378	377	adantr 482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
379	108	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
380	136	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
381		onsssuc 6452	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
382	129, 380, 381	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
383	146, 382	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ suc 𝑢)
384	52	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ dom 𝑂)
385		isorel 7320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
386	240, 384, 143, 385	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
387	243	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((◡𝑂‘𝑋) E suc 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢)
388	245	epeli 5582	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
389	386, 387, 388	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢)))
390	383, 389	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
391	379, 390	eqeltrrd 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
392		eleq2 2823	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ (𝑂‘suc 𝑢)))
393		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐹‘𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
394		fveq2 6889	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐺‘𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
395	393, 394	eqeq12d 2749	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
396	392, 395	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
397	396	rspcv 3609	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
398	202, 378, 391, 397	syl3c 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
399	398	oveq2d 7422	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))))
400	399	oveq1d 7421	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐺‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
401	376, 400	eqtr4d 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢)))
402	374, 401	eleq12d 2828	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑o (𝑂‘suc 𝑢)) ·o (𝐹‘(𝑂‘suc 𝑢))) +o (𝐻‘suc 𝑢))))
403	214, 402	bitr4d 282	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
404	403	biimpd 228	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
405	147, 404	embantd 59	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
406	405	expr 458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
407	140, 406	sylbird 260	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
408		fveq2 6889	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘suc 𝑢))
409	408	sseq2d 4014	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
410	409	ifbid 4551	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
411	410	mpteq2dv 5250	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
412	411	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
413		suceq 6428	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → suc (◡𝑂‘𝑋) = suc suc 𝑢)
414	413	fveq2d 6893	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc suc 𝑢))
415	412, 414	eleq12d 2828	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
416	115, 415	syl5ibcom 244	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
417	416	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
418	417	a1dd 50	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
419	407, 418	jaod 858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
420	134, 419	sylbid 239	. . . . . . . . 9 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
421	420	expimpd 455	. . . . . . . 8 ⊢ (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
422	421	com23 86	. . . . . . 7 ⊢ (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
423	422	a1i 11	. . . . . 6 ⊢ (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
424	82, 94, 106, 127, 423	finds2 7888	. . . . 5 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
425	70, 424	vtoclga 3566	. . . 4 ⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
426	57, 425	mpcom 38	. . 3 ⊢ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
427	44, 54, 426	mp2and 698	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))
428	155	feqmptd 6958	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)))
429		eqeq2 2745	. . . . . 6 ⊢ ((𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
430		eqeq2 2745	. . . . . 6 ⊢ (∅ = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
431		eqidd 2734	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = (𝐹‘𝑥))
432	199	ffvelcdmi 7083	. . . . . . . . . . . . . 14 ⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
433	44, 432	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
434	197, 433	sseldd 3983	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ 𝐵)
435		onelon 6387	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
436	10, 434, 435	syl2anc 585	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ On)
437	436	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
438		ontri1 6396	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
439	224, 437, 438	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
440	439	con2bid 355	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
441		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ 𝐵)
442	377	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
443		eloni 6372	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) ∈ On → Ord (◡𝑂‘𝑋))
444	129, 443	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ord (◡𝑂‘𝑋))
445		orduni 7774	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom 𝑂 → Ord ∪ dom 𝑂)
446	36, 445	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Ord ∪ dom 𝑂
447		ordtri1 6395	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord (◡𝑂‘𝑋) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
448	444, 446, 447	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
449	54, 448	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
450		isorel 7320	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
451	46, 44, 52, 450	syl12anc 836	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
452		fvex 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑂‘𝑋) ∈ V
453	452	epeli 5582	. . . . . . . . . . . . . . . . 17 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
454		fvex 6902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V
455	454	epeli 5582	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)))
456	451, 453, 455	3bitr3g 313	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋))))
457	108	eleq2d 2820	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
458	456, 457	bitrd 279	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
459	449, 458	mtbid 324	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋)
460		onelon 6387	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On)
461	10, 161, 460	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ On)
462		ontri1 6396	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
463	461, 436, 462	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
464	459, 463	mpbird 257	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
465	464	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
466		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
467	224	adantrr 716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
468		ontr2 6409	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
469	461, 467, 468	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
470	465, 466, 469	mp2and 698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ 𝑥)
471		eleq2 2823	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥))
472		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
473		fveq2 6889	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥))
474	472, 473	eqeq12d 2749	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
475	471, 474	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
476	475	rspcv 3609	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
477	441, 442, 470, 476	syl3c 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥))
478	466	adantr 482	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
479	46	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
480	44	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ dom 𝑂)
481	51	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
482		ffvelcdm 7081	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂:(𝐺 supp ∅)⟶dom 𝑂 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
483	481, 482	sylancom 589	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
484		isorel 7320	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
485	479, 480, 483, 484	syl12anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
486	269	epeli 5582	. . . . . . . . . . . . . . . 16 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
487	271	epeli 5582	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)))
488	485, 486, 487	3bitr3g 313	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥))))
489	48	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
490	489, 261	sylancom 589	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
491	490	eleq2d 2820	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
492	488, 491	bitrd 279	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
493	478, 492	mpbird 257	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
494		elssuni 4941	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑥) ∈ dom 𝑂 → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
495	483, 494	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
496	36, 483, 275	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ On)
497	496, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (◡𝑂‘𝑥))
498		ordtri1 6395	. . . . . . . . . . . . . . 15 ⊢ ((Ord (◡𝑂‘𝑥) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
499	497, 446, 498	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
500	495, 499	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
501	493, 500	pm2.65da 816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
502	441, 501	eldifd 3959	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
503		ssidd 4005	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
504	159, 503, 10, 176	suppssr 8178	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑥) = ∅)
505	502, 504	syldan 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐺‘𝑥) = ∅)
506	477, 505	eqtrd 2773	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = ∅)
507	506	expr 458	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 → (𝐹‘𝑥) = ∅))
508	440, 507	sylbird 260	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂) → (𝐹‘𝑥) = ∅))
509	508	imp 408	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = ∅)
510	429, 430, 431, 509	ifbothda 4566	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
511	510	mpteq2dva 5248	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
512	428, 511	eqtrd 2773	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
513	512	fveq2d 6893	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
514	8, 9, 10, 2, 13, 113	cantnfval 9660	. . 3 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
515	43	fveq2d 6893	. . 3 ⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom 𝑂))
516	514, 515	eqtrd 2773	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc ∪ dom 𝑂))
517	427, 513, 516	3eltr4d 2849	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  {crab 3433  Vcvv 3475   ∖ cdif 3945   ⊆ wss 3948  ∅c0 4322  ifcif 4528  ∪ cuni 4908   class class class wbr 5148  {copab 5210   ↦ cmpt 5231  Tr wtr 5265   E cep 5579   We wwe 5630  ^◡ccnv 5675  dom cdm 5676  Ord word 6361  Oncon0 6362  Lim wlim 6363  suc csuc 6364  Fun wfun 6535   Fn wfn 6536  ⟶wf 6537  –1-1-onto→wf1o 6540  ‘cfv 6541   Isom wiso 6542  (class class class)co 7406   ∈ cmpo 7408  ωcom 7852   supp csupp 8143  seq_ωcseqom 8444  1_oc1o 8456   +_o coa 8460   ·_o comu 8461   ↑_o coe 8462   ≈ cen 8933   finSupp cfsupp 9358  OrdIsocoi 9501   CNF ccnf 9653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-supp 8144  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-seqom 8445  df-1o 8463  df-2o 8464  df-oadd 8467  df-omul 8468  df-oexp 8469  df-er 8700  df-map 8819  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-oi 9502  df-cnf 9654

This theorem is referenced by:  cantnf  9685