Theorem cantnflem1 8469

Description: Lemma for cantnf 8473. 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 ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅)

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 6577	. . . . . 6 ⊢ (𝐺 supp ∅) ∈ V
2		cantnflem1.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
3	2	oion 8324	. . . . . 6 ⊢ ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
4	1, 3	mp1i 13	. . . . 5 ⊢ (𝜑 → dom 𝑂 ∈ On)
5		uniexg 6853	. . . . 5 ⊢ (dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V)
6		sucidg 5720	. . . . 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 8465	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
17		n0i 3879	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19		suppssdm 7195	. . . . . . . . . . . 12 ⊢ (𝐺 supp ∅) ⊆ dom 𝐺
20	8, 9, 10	cantnfs 8446	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)))
21	13, 20	mpbid 221	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))
22	21	simpld 474	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
23		fdm 5964	. . . . . . . . . . . . 13 ⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵)
24	22, 23	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → dom 𝐺 = 𝐵)
25	19, 24	syl5sseq 3616	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
26	10, 25	ssexd 4733	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 supp ∅) ∈ V)
27	8, 9, 10, 2, 13	cantnfcl 8447	. . . . . . . . . . 11 ⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
28	27	simpld 474	. . . . . . . . . 10 ⊢ (𝜑 → E We (𝐺 supp ∅))
29	2	oien 8326	. . . . . . . . . 10 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
30	26, 28, 29	syl2anc 691	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
31		breq1 4586	. . . . . . . . . 10 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
32		ensymb 7890	. . . . . . . . . . 11 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
33		en0 7905	. . . . . . . . . . 11 ⊢ ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
34	32, 33	bitri 263	. . . . . . . . . 10 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
35	31, 34	syl6bb 275	. . . . . . . . 9 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
36	30, 35	syl5ibcom 234	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
37	18, 36	mtod 188	. . . . . . 7 ⊢ (𝜑 → ¬ dom 𝑂 = ∅)
38	27	simprd 478	. . . . . . . 8 ⊢ (𝜑 → dom 𝑂 ∈ ω)
39		nnlim 6970	. . . . . . . 8 ⊢ (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
40	38, 39	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ Lim dom 𝑂)
41		ioran 510	. . . . . . 7 ⊢ (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
42	37, 40, 41	sylanbrc 695	. . . . . 6 ⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
43	2	oicl 8317	. . . . . . 7 ⊢ Ord dom 𝑂
44		unizlim 5761	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
45	43, 44	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
46	42, 45	mtbird 314	. . . . 5 ⊢ (𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂)
47		orduniorsuc 6922	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
48	43, 47	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
49	48	ord 391	. . . . 5 ⊢ (𝜑 → (¬ dom 𝑂 = ∪ dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂))
50	46, 49	mpd 15	. . . 4 ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂)
51	7, 50	eleqtrrd 2691	. . 3 ⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂)
52	2	oiiso 8325	. . . . . . . 8 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
53	26, 28, 52	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
54		isof1o 6473	. . . . . . 7 ⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
55	53, 54	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
56		f1ocnv 6062	. . . . . 6 ⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
57		f1of 6050	. . . . . 6 ⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
58	55, 56, 57	3syl 18	. . . . 5 ⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
59	58, 16	ffvelrnd 6268	. . . 4 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂)
60		elssuni 4403	. . . 4 ⊢ ((◡𝑂‘𝑋) ∈ dom 𝑂 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
61	59, 60	syl 17	. . 3 ⊢ (𝜑 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
62	50, 38	eqeltrrd 2689	. . . . 5 ⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω)
63		peano2b 6973	. . . . 5 ⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω)
64	62, 63	sylibr 223	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ ω)
65		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂))
66		sseq2 3590	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂))
67	65, 66	anbi12d 743	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)))
68		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑂‘𝑦) = (𝑂‘∪ dom 𝑂))
69	68	sseq2d 3596	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
70	69	ifbid 4058	. . . . . . . . . 10 ⊢ (𝑦 = ∪ dom 𝑂 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
71	70	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
72	71	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
73		suceq 5707	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂)
74	73	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc ∪ dom 𝑂))
75	72, 74	eleq12d 2682	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
76	67, 75	imbi12d 333	. . . . . 6 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
77	76	imbi2d 329	. . . . 5 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))))
78		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
79		sseq2 3590	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∅))
80	78, 79	anbi12d 743	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅)))
81		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (𝑂‘𝑦) = (𝑂‘∅))
82	81	sseq2d 3596	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
83	82	ifbid 4058	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
84	83	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
85	84	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
86		suceq 5707	. . . . . . . . 9 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
87	86	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
88	85, 87	eleq12d 2682	. . . . . . 7 ⊢ (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
89	80, 88	imbi12d 333	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅))))
90		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂))
91		sseq2 3590	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ 𝑢))
92	90, 91	anbi12d 743	. . . . . . 7 ⊢ (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)))
93		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑂‘𝑦) = (𝑂‘𝑢))
94	93	sseq2d 3596	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘𝑢)))
95	94	ifbid 4058	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
96	95	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
97	96	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))
98		suceq 5707	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
99	98	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
100	97, 99	eleq12d 2682	. . . . . . 7 ⊢ (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
101	92, 100	imbi12d 333	. . . . . 6 ⊢ (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
102		eleq1 2676	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
103		sseq2 3590	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ suc 𝑢))
104	102, 103	anbi12d 743	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢)))
105		fveq2 6103	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑢 → (𝑂‘𝑦) = (𝑂‘suc 𝑢))
106	105	sseq2d 3596	. . . . . . . . . . 11 ⊢ (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
107	106	ifbid 4058	. . . . . . . . . 10 ⊢ (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
108	107	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
109	108	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
110		suceq 5707	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
111	110	fveq2d 6107	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
112	109, 111	eleq12d 2682	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
113	104, 112	imbi12d 333	. . . . . 6 ⊢ (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
114		f1ocnvfv2 6433	. . . . . . . . . . . . 13 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
115	55, 16, 114	syl2anc 691	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
116	115	sseq2d 3596	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ 𝑋))
117	116	ifbid 4058	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))
118	117	mpteq2dv 4673	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)))
119	118	fveq2d 6107	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))))
120		cantnflem1.h	. . . . . . . . 9 ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅)
121	8, 9, 10, 11, 12, 13, 14, 15, 2, 120	cantnflem1d 8468	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
122	119, 121	eqeltrd 2688	. . . . . . 7 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
123		ss0 3926	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (◡𝑂‘𝑋) = ∅)
124	123	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘∅))
125	124	sseq2d 3596	. . . . . . . . . . . 12 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
126	125	ifbid 4058	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
127	126	mpteq2dv 4673	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
128	127	fveq2d 6107	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
129		suceq 5707	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) = ∅ → suc (◡𝑂‘𝑋) = suc ∅)
130	123, 129	syl 17	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → suc (◡𝑂‘𝑋) = suc ∅)
131	130	fveq2d 6107	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc ∅))
132	128, 131	eleq12d 2682	. . . . . . . 8 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
133	132	adantl 481	. . . . . . 7 ⊢ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
134	122, 133	syl5ibcom 234	. . . . . 6 ⊢ (𝜑 → ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
135		ordelon 5664	. . . . . . . . . . . . 13 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On)
136	43, 59, 135	sylancr 694	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On)
137	136	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On)
138	43	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord dom 𝑂)
139		ordelon 5664	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
140	138, 139	sylan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
141		onsseleq 5682	. . . . . . . . . . 11 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
142	137, 140, 141	syl2anc 691	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
143		sucelon 6909	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
144	140, 143	sylibr 223	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
145		eloni 5650	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ On → Ord 𝑢)
146	144, 145	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
147		ordsssuc 5729	. . . . . . . . . . . . 13 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ Ord 𝑢) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
148	137, 146, 147	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
149		ordtr 5654	. . . . . . . . . . . . . . . . 17 ⊢ (Ord dom 𝑂 → Tr dom 𝑂)
150	43, 149	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
151		simprl 790	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
152		trsuc 5727	. . . . . . . . . . . . . . . 16 ⊢ ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
153	150, 151, 152	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
154		simprr 792	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ⊆ 𝑢)
155	153, 154	jca 553	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢))
156	9	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
157	10	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
158		oecl 7504	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 𝐵) ∈ On)
159	156, 157, 158	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑𝑜 𝐵) ∈ On)
160	8, 156, 157	cantnff 8454	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵))
161	8, 9, 10	cantnfs 8446	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
162	12, 161	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
163	162	simpld 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
164	163	ffvelrnda 6267	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) ∈ 𝐴)
165	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 8464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
166	165	simp1d 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
167	22, 166	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
168		ne0i 3880	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑋) ∈ 𝐴 → 𝐴 ≠ ∅)
169	167, 168	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ≠ ∅)
170		on0eln0 5697	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
171	9, 170	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
172	169, 171	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∅ ∈ 𝐴)
173	172	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∅ ∈ 𝐴)
174	164, 173	ifcld 4081	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ 𝐴)
175		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
176	174, 175	fmptd 6292	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴)
177		mptexg 6389	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
178	10, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
179		funmpt 5840	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
180	179	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
181	162	simprd 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 finSupp ∅)
182		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 supp ∅) = (𝐹 supp ∅)
183		eqimss2 3621	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 supp ∅) = (𝐹 supp ∅) → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
184	182, 183	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
185		0ex 4718	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ V
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∅ ∈ V)
187	163, 184, 10, 186	suppssr 7213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑥) = ∅)
188	187	ifeq1d 4054	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
189		ifid 4075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅) = ∅
190	188, 189	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
191	190, 10	suppss2 7216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
192		fsuppsssupp 8174	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V ∧ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
193	178, 180, 181, 191, 192	syl22anc 1319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
194	8, 9, 10	cantnfs 8446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)))
195	176, 193, 194	mpbir2and 959	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
196	195	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
197	160, 196	ffvelrnd 6268	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑𝑜 𝐵))
198		onelon 5665	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
199	159, 197, 198	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
200	38	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
201		elnn 6967	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
202	151, 200, 201	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
203	120	cantnfvalf 8445	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻:ω⟶On
204	203	ffvelrni 6266	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
205	202, 204	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
206	25	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
207	2	oif 8318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅)
208	207	ffvelrni 6266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
209	151, 208	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
210	206, 209	sseldd 3569	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
211		onelon 5665	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
212	157, 210, 211	syl2anc 691	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
213		oecl 7504	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On)
214	156, 212, 213	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On)
215	163	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐹:𝐵⟶𝐴)
216	215, 210	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
217		onelon 5665	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
218	156, 216, 217	syl2anc 691	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
219		omcl 7503	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
220	214, 218, 219	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
221		oaord 7514	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
222	199, 205, 220, 221	syl3anc 1318	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
223		ifeq1 4040	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
224		ifid 4075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
225	223, 224	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = ∅)
226		ifeq1 4040	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅))
227		ifid 4075	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅) = ∅
228	226, 227	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = ∅)
229	225, 228	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) ↔ ∅ = ∅))
230		onss 6882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
231	10, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ⊆ On)
232	231	sselda 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
233	232	adantlr 747	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
234	212	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
235		onsseleq 5682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
236	233, 234, 235	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
237	236	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
238	233	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → 𝑥 ∈ On)
239	207	ffvelrni 6266	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
240	153, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
241	206, 240	sseldd 3569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵)
242		onelon 5665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On)
243	157, 241, 242	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On)
244	243	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑂‘𝑢) ∈ On)
245		onsssuc 5730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
246	238, 244, 245	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
247		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑢 ∈ V
248	247	sucid 5721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ suc 𝑢
249	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
250		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
251	249, 153, 151, 250	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
252	247	sucex 6903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ suc 𝑢 ∈ V
253	252	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢)
254		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑂‘suc 𝑢) ∈ V
255	254	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
256	251, 253, 255	3bitr3g 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢)))
257	248, 256	mpbii 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
258		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
259	212, 258	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
260		ordelsuc 6912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑂‘𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
261	243, 259, 260	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
262	257, 261	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
263	262	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
264	263	sseld 3567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
265	246, 264	sylbid 229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
266		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥)
267	249	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
268	267, 54	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
269	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 8467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
270		f1ocnvfv2 6433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
271	268, 269, 270	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
272	266, 271	eleqtrrd 2691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
273	153	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
274	268, 56, 57	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
275	274, 269	ffvelrnd 6268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
276		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
277	267, 273, 275, 276	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
278		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡𝑂‘𝑥) ∈ V
279	278	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 E (◡𝑂‘𝑥) ↔ 𝑢 ∈ (◡𝑂‘𝑥))
280		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑂‘(◡𝑂‘𝑥)) ∈ V
281	280	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
282	277, 279, 281	3bitr3g 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥))))
283	272, 282	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ (◡𝑂‘𝑥))
284		ordelon 5664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂) → (◡𝑂‘𝑥) ∈ On)
285	43, 275, 284	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ On)
286		eloni 5650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((◡𝑂‘𝑥) ∈ On → Ord (◡𝑂‘𝑥))
287	285, 286	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → Ord (◡𝑂‘𝑥))
288		ordelsuc 6912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ (◡𝑂‘𝑥) ∧ Ord (◡𝑂‘𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
289	283, 287, 288	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
290	283, 289	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (◡𝑂‘𝑥))
291	151	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
292	43, 291, 139	sylancr 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
293		ontri1 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((suc 𝑢 ∈ On ∧ (◡𝑂‘𝑥) ∈ On) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
294	292, 285, 293	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
295	290, 294	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ (◡𝑂‘𝑥) ∈ suc 𝑢)
296		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
297	267, 275, 291, 296	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
298	252	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((◡𝑂‘𝑥) E suc 𝑢 ↔ (◡𝑂‘𝑥) ∈ suc 𝑢)
299	254	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢))
300	297, 298, 299	3bitr3g 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢)))
301	271	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
302	300, 301	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
303	295, 302	mtbid 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
304	303	expr 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑂‘𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
305	304	con2d 128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂‘𝑢) ∈ 𝑥))
306		ontri1 5674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
307	238, 244, 306	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
308	305, 307	sylibrd 248	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂‘𝑢)))
309	265, 308	impbid 201	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
310	309	orbi1d 735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
311	237, 310	bitr4d 270	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
312		orcom 401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)))
313	311, 312	syl6bb 275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢))))
314	313	ifbid 4058	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
315		eqidd 2611	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ∅ = ∅)
316	229, 314, 315	pm2.61ne 2867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
317	316	mpteq2dva 4672	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)))
318	317	fveq2d 6107	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))))
319		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑥) ∈ V
320	319, 185	ifex 4106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
322	321	ralrimivw 2950	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
323	175	fnmpt 5933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
324	322, 323	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
325	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∅ ∈ V)
326		suppvalfn 7189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅})
327		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝐵
328		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥𝐵
329		nffvmpt1 6111	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)
330		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥∅
331	329, 330	nfne 2882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅
332		nfv 1830	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅
333		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥))
334	333	neeq1d 2841	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅))
335	327, 328, 331, 332, 334	cbvrab 3171	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅}
336	326, 335	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
337	324, 157, 325, 336	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
338		eqidd 2611	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
339	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
340	338, 339	fvmpt2d 6202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
341	340	neeq1d 2841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
342	339	biantrurd 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)))
343		dif1o 7467	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
344	342, 343	syl6bbr 277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)))
345	341, 344	bitrd 267	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)))
346	345	rabbidva 3163	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)})
347	337, 346	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)})
348	320, 343	mpbiran 955	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)
349		ifeq1 4040	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
350	349, 189	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
351	350	necon3i 2814	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → (𝐹‘𝑥) ≠ ∅)
352		iffalse 4045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ⊆ (𝑂‘𝑢) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
353	352	necon1ai 2809	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂‘𝑢))
354	351, 353	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → ((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)))
355	265	expimpd 627	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
356	354, 355	syl5 33	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
357	348, 356	syl5bi 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) → 𝑥 ∈ (𝑂‘suc 𝑢)))
358	357	3impia 1253	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵 ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
359	358	rabssdv 3645	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
360	347, 359	eqsstrd 3602	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
361		eqeq1 2614	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
362		sseq1 3589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑦 ⊆ (𝑂‘𝑢)))
363	361, 362	orbi12d 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢))))
364		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
365	363, 364	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
366	365	cbvmptv 4678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
367		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑂‘suc 𝑢) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
368	367	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 = (𝑂‘suc 𝑢)) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
369	368	ifeq1da 4066	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
370	362, 364	ifbieq1d 4059	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
371		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑦) ∈ V
372	371, 185	ifex 4106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅) ∈ V
373	370, 175, 372	fvmpt 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
374	373	ifeq2d 4055	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅)))
375		ifor 4085	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
376	374, 375	syl6eqr 2662	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
377	369, 376	eqtr3d 2646	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
378	377	mpteq2ia 4668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
379	366, 378	eqtr4i 2635	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
380	8, 156, 157, 196, 210, 216, 360, 379	cantnfp1 8461	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))))
381	380	simprd 478	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
382	318, 381	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
383	8, 9, 10, 2, 13, 120	cantnfsuc 8450	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
384	202, 383	syldan 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
385	165	simp3d 1068	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
386	385	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
387	115	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
388	136	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ On)
389	144	adantrr 749	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
390		onsssuc 5730	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
391	388, 389, 390	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
392	154, 391	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ suc 𝑢)
393	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ dom 𝑂)
394		isorel 6476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
395	249, 393, 151, 394	syl12anc 1316	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
396	252	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((◡𝑂‘𝑋) E suc 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢)
397	254	epelc 4951	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
398	395, 396, 397	3bitr3g 301	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢)))
399	392, 398	mpbid 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
400	387, 399	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
401		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ (𝑂‘suc 𝑢)))
402		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐹‘𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
403		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐺‘𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
404	402, 403	eqeq12d 2625	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
405	401, 404	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
406	405	rspcv 3278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
407	210, 386, 400, 406	syl3c 64	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
408	407	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
409	408	oveq1d 6564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
410	384, 409	eqtr4d 2647	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
411	382, 410	eleq12d 2682	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
412	222, 411	bitr4d 270	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
413	412	biimpd 218	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
414	155, 413	embantd 57	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
415	414	expr 641	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
416	148, 415	sylbird 249	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
417		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘suc 𝑢))
418	417	sseq2d 3596	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
419	418	ifbid 4058	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
420	419	mpteq2dv 4673	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
421	420	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
422		suceq 5707	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → suc (◡𝑂‘𝑋) = suc suc 𝑢)
423	422	fveq2d 6107	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc suc 𝑢))
424	421, 423	eleq12d 2682	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
425	122, 424	syl5ibcom 234	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
426	425	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
427	426	a1dd 48	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
428	416, 427	jaod 394	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
429	142, 428	sylbid 229	. . . . . . . . 9 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
430	429	expimpd 627	. . . . . . . 8 ⊢ (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
431	430	com23 84	. . . . . . 7 ⊢ (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
432	431	a1i 11	. . . . . 6 ⊢ (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
433	89, 101, 113, 134, 432	finds2 6986	. . . . 5 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
434	77, 433	vtoclga 3245	. . . 4 ⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
435	64, 434	mpcom 37	. . 3 ⊢ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
436	51, 61, 435	mp2and 711	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))
437	163	feqmptd 6159	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)))
438		eqeq2 2621	. . . . . 6 ⊢ ((𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
439		eqeq2 2621	. . . . . 6 ⊢ (∅ = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
440		eqidd 2611	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = (𝐹‘𝑥))
441	207	ffvelrni 6266	. . . . . . . . . . . . . 14 ⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
442	51, 441	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
443	25, 442	sseldd 3569	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ 𝐵)
444		onelon 5665	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
445	10, 443, 444	syl2anc 691	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ On)
446	445	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
447		ontri1 5674	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
448	232, 446, 447	syl2anc 691	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
449	448	con2bid 343	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
450		simprl 790	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ 𝐵)
451	385	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
452		eloni 5650	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) ∈ On → Ord (◡𝑂‘𝑋))
453	136, 452	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ord (◡𝑂‘𝑋))
454		orduni 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom 𝑂 → Ord ∪ dom 𝑂)
455	43, 454	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Ord ∪ dom 𝑂
456		ordtri1 5673	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord (◡𝑂‘𝑋) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
457	453, 455, 456	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
458	61, 457	mpbid 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
459		isorel 6476	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
460	53, 51, 59, 459	syl12anc 1316	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
461		fvex 6113	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑂‘𝑋) ∈ V
462	461	epelc 4951	. . . . . . . . . . . . . . . . 17 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
463		fvex 6113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V
464	463	epelc 4951	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)))
465	460, 462, 464	3bitr3g 301	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋))))
466	115	eleq2d 2673	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
467	465, 466	bitrd 267	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
468	458, 467	mtbid 313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋)
469		onelon 5665	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On)
470	10, 166, 469	syl2anc 691	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ On)
471		ontri1 5674	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
472	470, 445, 471	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
473	468, 472	mpbird 246	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
474	473	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
475		simprr 792	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
476	470	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
477	232	adantrr 749	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
478		ontr2 5689	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
479	476, 477, 478	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
480	474, 475, 479	mp2and 711	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ 𝑥)
481		eleq2 2677	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥))
482		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
483		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥))
484	482, 483	eqeq12d 2625	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
485	481, 484	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
486	485	rspcv 3278	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
487	450, 451, 480, 486	syl3c 64	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥))
488	475	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
489	53	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
490	51	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ dom 𝑂)
491	58	ad2antrr 758	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
492		ffvelrn 6265	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂:(𝐺 supp ∅)⟶dom 𝑂 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
493	491, 492	sylancom 698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
494		isorel 6476	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
495	489, 490, 493, 494	syl12anc 1316	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
496	278	epelc 4951	. . . . . . . . . . . . . . . 16 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
497	280	epelc 4951	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)))
498	495, 496, 497	3bitr3g 301	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥))))
499	55	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
500	499, 270	sylancom 698	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
501	500	eleq2d 2673	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
502	498, 501	bitrd 267	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
503	488, 502	mpbird 246	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
504		elssuni 4403	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑥) ∈ dom 𝑂 → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
505	493, 504	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
506	43, 493, 284	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ On)
507	506, 286	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (◡𝑂‘𝑥))
508		ordtri1 5673	. . . . . . . . . . . . . . 15 ⊢ ((Ord (◡𝑂‘𝑥) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
509	507, 455, 508	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
510	505, 509	mpbid 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
511	503, 510	pm2.65da 598	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
512	450, 511	eldifd 3551	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
513		ssid 3587	. . . . . . . . . . . . 13 ⊢ (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
514	513	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
515	22, 514, 10, 186	suppssr 7213	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑥) = ∅)
516	512, 515	syldan 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐺‘𝑥) = ∅)
517	487, 516	eqtrd 2644	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = ∅)
518	517	expr 641	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 → (𝐹‘𝑥) = ∅))
519	449, 518	sylbird 249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂) → (𝐹‘𝑥) = ∅))
520	519	imp 444	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = ∅)
521	438, 439, 440, 520	ifbothda 4073	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
522	521	mpteq2dva 4672	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
523	437, 522	eqtrd 2644	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
524	523	fveq2d 6107	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
525	8, 9, 10, 2, 13, 120	cantnfval 8448	. . 3 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
526	50	fveq2d 6107	. . 3 ⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom 𝑂))
527	525, 526	eqtrd 2644	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc ∪ dom 𝑂))
528	436, 524, 527	3eltr4d 2703	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874  ifcif 4036  ∪ cuni 4372   class class class wbr 4583  {copab 4642   ↦ cmpt 4643  Tr wtr 4680   E cep 4947   We wwe 4996  ^◡ccnv 5037  dom cdm 5038  Ord word 5639  Oncon0 5640  Lim wlim 5641  suc csuc 5642  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549   ↦ cmpt2 6551  ωcom 6957   supp csupp 7182  seq_𝜔cseqom 7429  1_𝑜c1o 7440   +_𝑜 coa 7444   ·_𝑜 comu 7445   ↑_𝑜 coe 7446   ≈ cen 7838   finSupp cfsupp 8158  OrdIsocoi 8297   CNF ccnf 8441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-supp 7183  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-seqom 7430  df-1o 7447  df-2o 7448  df-oadd 7451  df-omul 7452  df-oexp 7453  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fsupp 8159  df-oi 8298  df-cnf 8442

This theorem is referenced by:  cantnf  8473