Theorem cantnflem1 8624

Description: Lemma for cantnf 8628. 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 6718	. . . . . 6 ⊢ (𝐺 supp ∅) ∈ V
2		cantnflem1.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
3	2	oion 8482	. . . . . 6 ⊢ ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
4	1, 3	mp1i 13	. . . . 5 ⊢ (𝜑 → dom 𝑂 ∈ On)
5		uniexg 6997	. . . . 5 ⊢ (dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V)
6		sucidg 5841	. . . . 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 8620	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
17		n0i 3953	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19		ovexd 6720	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 supp ∅) ∈ V)
20	8, 9, 10, 2, 13	cantnfcl 8602	. . . . . . . . . . 11 ⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
21	20	simpld 474	. . . . . . . . . 10 ⊢ (𝜑 → E We (𝐺 supp ∅))
22	2	oien 8484	. . . . . . . . . 10 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
23	19, 21, 22	syl2anc 694	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24		breq1 4688	. . . . . . . . . 10 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25		ensymb 8045	. . . . . . . . . . 11 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26		en0 8060	. . . . . . . . . . 11 ⊢ ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
27	25, 26	bitri 264	. . . . . . . . . 10 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
28	24, 27	syl6bb 276	. . . . . . . . 9 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
29	23, 28	syl5ibcom 235	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
30	18, 29	mtod 189	. . . . . . 7 ⊢ (𝜑 → ¬ dom 𝑂 = ∅)
31	20	simprd 478	. . . . . . . 8 ⊢ (𝜑 → dom 𝑂 ∈ ω)
32		nnlim 7120	. . . . . . . 8 ⊢ (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
33	31, 32	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ Lim dom 𝑂)
34		ioran 510	. . . . . . 7 ⊢ (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
35	30, 33, 34	sylanbrc 699	. . . . . 6 ⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
36	2	oicl 8475	. . . . . . 7 ⊢ Ord dom 𝑂
37		unizlim 5882	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
38	36, 37	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
39	35, 38	mtbird 314	. . . . 5 ⊢ (𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂)
40		orduniorsuc 7072	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
41	36, 40	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
42	41	ord 391	. . . . 5 ⊢ (𝜑 → (¬ dom 𝑂 = ∪ dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂))
43	39, 42	mpd 15	. . . 4 ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂)
44	7, 43	eleqtrrd 2733	. . 3 ⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂)
45	2	oiiso 8483	. . . . . . . 8 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
46	19, 21, 45	syl2anc 694	. . . . . . 7 ⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47		isof1o 6613	. . . . . . 7 ⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
48	46, 47	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
49		f1ocnv 6187	. . . . . 6 ⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50		f1of 6175	. . . . . 6 ⊢ (◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
51	48, 49, 50	3syl 18	. . . . 5 ⊢ (𝜑 → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
52	51, 16	ffvelrnd 6400	. . . 4 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ dom 𝑂)
53		elssuni 4499	. . . 4 ⊢ ((◡𝑂‘𝑋) ∈ dom 𝑂 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . 3 ⊢ (𝜑 → (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
55	43, 31	eqeltrrd 2731	. . . . 5 ⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω)
56		peano2b 7123	. . . . 5 ⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω)
57	55, 56	sylibr 224	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ ω)
58		eleq1 2718	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂))
59		sseq2 3660	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂))
60	58, 59	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)))
61		fveq2 6229	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑂‘𝑦) = (𝑂‘∪ dom 𝑂))
62	61	sseq2d 3666	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
63	62	ifbid 4141	. . . . . . . . . 10 ⊢ (𝑦 = ∪ dom 𝑂 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
64	63	mpteq2dv 4778	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
65	64	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
66		suceq 5828	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂)
67	66	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc ∪ dom 𝑂))
68	65, 67	eleq12d 2724	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
69	60, 68	imbi12d 333	. . . . . 6 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
70	69	imbi2d 329	. . . . 5 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))))
71		eleq1 2718	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72		sseq2 3660	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ ∅))
73	71, 72	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅)))
74		fveq2 6229	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (𝑂‘𝑦) = (𝑂‘∅))
75	74	sseq2d 3666	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
76	75	ifbid 4141	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
77	76	mpteq2dv 4778	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
78	77	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
79		suceq 5828	. . . . . . . . 9 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
80	79	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
81	78, 80	eleq12d 2724	. . . . . . 7 ⊢ (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
82	73, 81	imbi12d 333	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83		eleq1 2718	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂))
84		sseq2 3660	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ 𝑢))
85	83, 84	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)))
86		fveq2 6229	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑂‘𝑦) = (𝑂‘𝑢))
87	86	sseq2d 3666	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘𝑢)))
88	87	ifbid 4141	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
89	88	mpteq2dv 4778	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
90	89	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))
91		suceq 5828	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
92	91	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
93	90, 92	eleq12d 2724	. . . . . . 7 ⊢ (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
94	85, 93	imbi12d 333	. . . . . 6 ⊢ (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95		eleq1 2718	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96		sseq2 3660	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((◡𝑂‘𝑋) ⊆ 𝑦 ↔ (◡𝑂‘𝑋) ⊆ suc 𝑢))
97	95, 96	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢)))
98		fveq2 6229	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑢 → (𝑂‘𝑦) = (𝑂‘suc 𝑢))
99	98	sseq2d 3666	. . . . . . . . . . 11 ⊢ (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
100	99	ifbid 4141	. . . . . . . . . 10 ⊢ (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
101	100	mpteq2dv 4778	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
102	101	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
103		suceq 5828	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104	103	fveq2d 6233	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105	102, 104	eleq12d 2724	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
106	97, 105	imbi12d 333	. . . . . 6 ⊢ (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107		f1ocnvfv2 6573	. . . . . . . . . . . . 13 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
108	48, 16, 107	syl2anc 694	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
109	108	sseq2d 3666	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ 𝑋))
110	109	ifbid 4141	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))
111	110	mpteq2dv 4778	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)))
112	111	fveq2d 6233	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))))
113		cantnflem1.h	. . . . . . . . 9 ⊢ 𝐻 = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (𝑂‘𝑘)) ·𝑜 (𝐺‘(𝑂‘𝑘))) +𝑜 𝑧)), ∅)
114	8, 9, 10, 11, 12, 13, 14, 15, 2, 113	cantnflem1d 8623	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
115	112, 114	eqeltrd 2730	. . . . . . 7 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)))
116		ss0 4007	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (◡𝑂‘𝑋) = ∅)
117	116	fveq2d 6233	. . . . . . . . . . . . 13 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘∅))
118	117	sseq2d 3666	. . . . . . . . . . . 12 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119	118	ifbid 4141	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
120	119	mpteq2dv 4778	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
121	120	fveq2d 6233	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
122		suceq 5828	. . . . . . . . . . 11 ⊢ ((◡𝑂‘𝑋) = ∅ → suc (◡𝑂‘𝑋) = suc ∅)
123	116, 122	syl 17	. . . . . . . . . 10 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → suc (◡𝑂‘𝑋) = suc ∅)
124	123	fveq2d 6233	. . . . . . . . 9 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc ∅))
125	121, 124	eleq12d 2724	. . . . . . . 8 ⊢ ((◡𝑂‘𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126	125	adantl 481	. . . . . . 7 ⊢ ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127	115, 126	syl5ibcom 235	. . . . . 6 ⊢ (𝜑 → ((∅ ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128		ordelon 5785	. . . . . . . . . . . . 13 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On)
129	36, 52, 128	sylancr 696	. . . . . . . . . . . 12 ⊢ (𝜑 → (◡𝑂‘𝑋) ∈ On)
130	129	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (◡𝑂‘𝑋) ∈ On)
131	36	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord dom 𝑂)
132		ordelon 5785	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133	131, 132	sylan 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
134		onsseleq 5803	. . . . . . . . . . 11 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
135	130, 133, 134	syl2anc 694	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (◡𝑂‘𝑋) = suc 𝑢)))
136		sucelon 7059	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
137	133, 136	sylibr 224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
138		eloni 5771	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ On → Ord 𝑢)
139	137, 138	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
140		ordsssuc 5850	. . . . . . . . . . . . 13 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ Ord 𝑢) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
141	130, 139, 140	syl2anc 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
142		ordtr 5775	. . . . . . . . . . . . . . . . 17 ⊢ (Ord dom 𝑂 → Tr dom 𝑂)
143	36, 142	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
144		simprl 809	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
145		trsuc 5848	. . . . . . . . . . . . . . . 16 ⊢ ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
146	143, 144, 145	syl2anc 694	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
147		simprr 811	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ⊆ 𝑢)
148	146, 147	jca 553	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢))
149	9	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
150	10	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
151		oecl 7662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜 𝐵) ∈ On)
152	149, 150, 151	syl2anc 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑𝑜 𝐵) ∈ On)
153	8, 149, 150	cantnff 8609	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵))
154	8, 9, 10	cantnfs 8601	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
155	12, 154	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
156	155	simpld 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
157	156	ffvelrnda 6399	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) ∈ 𝐴)
158	8, 9, 10	cantnfs 8601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)))
159	13, 158	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))
160	159	simpld 474	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
161	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 8619	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
162	161	simp1d 1093	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
163	160, 162	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
164		ne0i 3954	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐺‘𝑋) ∈ 𝐴 → 𝐴 ≠ ∅)
165	163, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ≠ ∅)
166		on0eln0 5818	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
167	9, 166	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
168	165, 167	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∅ ∈ 𝐴)
169	168	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∅ ∈ 𝐴)
170	157, 169	ifcld 4164	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ 𝐴)
171		eqid 2651	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
172	170, 171	fmptd 6425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴)
173		mptexg 6525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐵 ∈ On → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
174	10, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
175		funmpt 5964	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
177	155	simprd 478	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 finSupp ∅)
178		eqid 2651	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹 supp ∅) = (𝐹 supp ∅)
179		eqimss2 3691	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹 supp ∅) = (𝐹 supp ∅) → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
180	178, 179	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
181		0ex 4823	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ V
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∅ ∈ V)
183	156, 180, 10, 182	suppssr 7371	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑥) = ∅)
184	183	ifeq1d 4137	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
185		ifid 4158	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅) = ∅
186	184, 185	syl6eq 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
187	186, 10	suppss2 7374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
188		fsuppsssupp 8332	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V ∧ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
189	174, 176, 177, 187, 188	syl22anc 1367	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
190	8, 9, 10	cantnfs 8601	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)))
191	172, 189, 190	mpbir2and 977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
192	191	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
193	153, 192	ffvelrnd 6400	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑𝑜 𝐵))
194		onelon 5786	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑𝑜 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑𝑜 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
195	152, 193, 194	syl2anc 694	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
196	31	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
197		elnn 7117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
198	144, 196, 197	syl2anc 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
199	113	cantnfvalf 8600	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻:ω⟶On
200	199	ffvelrni 6398	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
201	198, 200	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
202		suppssdm 7353	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 supp ∅) ⊆ dom 𝐺
203		fdm 6089	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐺:𝐵⟶𝐴 → dom 𝐺 = 𝐵)
204	160, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → dom 𝐺 = 𝐵)
205	202, 204	syl5sseq 3686	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
206	205	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
207	2	oif 8476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅)
208	207	ffvelrni 6398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
209	144, 208	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
210	206, 209	sseldd 3637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
211		onelon 5786	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
212	150, 210, 211	syl2anc 694	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
213		oecl 7662	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On)
214	149, 212, 213	syl2anc 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On)
215	156	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐹:𝐵⟶𝐴)
216	215, 210	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
217		onelon 5786	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
218	149, 216, 217	syl2anc 694	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
219		omcl 7661	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
220	214, 218, 219	syl2anc 694	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
221		oaord 7672	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
222	195, 201, 220, 221	syl3anc 1366	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
223		ifeq1 4123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
224		ifid 4158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
225	223, 224	syl6eq 2701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = ∅)
226		ifeq1 4123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅))
227		ifid 4158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅) = ∅
228	226, 227	syl6eq 2701	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = ∅)
229	225, 228	eqeq12d 2666	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) ↔ ∅ = ∅))
230		onss 7032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
231	10, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ⊆ On)
232	231	sselda 3636	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
233	232	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
234	212	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
235		onsseleq 5803	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
236	233, 234, 235	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . 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 6398	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
240	146, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
241	206, 240	sseldd 3637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵)
242		onelon 5786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On)
243	150, 241, 242	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On)
244	243	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑂‘𝑢) ∈ On)
245		onsssuc 5851	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
246	238, 244, 245	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
247		vex 3234	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑢 ∈ V
248	247	sucid 5842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ suc 𝑢
249	46	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
250		isorel 6616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
251	249, 146, 144, 250	syl12anc 1364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
252	247	sucex 7053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ suc 𝑢 ∈ V
253	252	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢)
254		fvex 6239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑂‘suc 𝑢) ∈ V
255	254	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
256	251, 253, 255	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢)))
257	248, 256	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
258		eloni 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
259	212, 258	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
260		ordelsuc 7062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑂‘𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
261	243, 259, 260	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
262	257, 261	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
263	262	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
264	263	sseld 3635	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
265	246, 264	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
266		simprr 811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥)
267	249	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
268	267, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
269	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 8622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
270		f1ocnvfv2 6573	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
271	268, 269, 270	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
272	266, 271	eleqtrrd 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
273	146	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
274	268, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
275	274, 269	ffvelrnd 6400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
276		isorel 6616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
277	267, 273, 275, 276	syl12anc 1364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 E (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥))))
278		fvex 6239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (◡𝑂‘𝑥) ∈ V
279	278	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 E (◡𝑂‘𝑥) ↔ 𝑢 ∈ (◡𝑂‘𝑥))
280		fvex 6239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑂‘(◡𝑂‘𝑥)) ∈ V
281	280	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑂‘𝑢) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥)))
282	277, 279, 281	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘𝑢) ∈ (𝑂‘(◡𝑂‘𝑥))))
283	272, 282	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ (◡𝑂‘𝑥))
284		ordelon 5785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((Ord dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂) → (◡𝑂‘𝑥) ∈ On)
285	36, 275, 284	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (◡𝑂‘𝑥) ∈ On)
286		eloni 5771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((◡𝑂‘𝑥) ∈ On → Ord (◡𝑂‘𝑥))
287	285, 286	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → Ord (◡𝑂‘𝑥))
288		ordelsuc 7062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ (◡𝑂‘𝑥) ∧ Ord (◡𝑂‘𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
289	283, 287, 288	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (◡𝑂‘𝑥)))
290	283, 289	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (◡𝑂‘𝑥))
291	144	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
292	36, 291, 132	sylancr 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
293		ontri1 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((suc 𝑢 ∈ On ∧ (◡𝑂‘𝑥) ∈ On) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
294	292, 285, 293	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (◡𝑂‘𝑥) ↔ ¬ (◡𝑂‘𝑥) ∈ suc 𝑢))
295	290, 294	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ (◡𝑂‘𝑥) ∈ suc 𝑢)
296		isorel 6616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
297	267, 275, 291, 296	syl12anc 1364	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
298	252	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((◡𝑂‘𝑥) E suc 𝑢 ↔ (◡𝑂‘𝑥) ∈ suc 𝑢)
299	254	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘(◡𝑂‘𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢))
300	297, 298, 299	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢)))
301	271	eleq1d 2715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑂‘(◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
302	300, 301	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((◡𝑂‘𝑥) ∈ suc 𝑢 ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
303	295, 302	mtbid 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
304	303	expr 642	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑂‘𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
305	304	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂‘𝑢) ∈ 𝑥))
306		ontri1 5795	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
307	238, 244, 306	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
308	305, 307	sylibrd 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂‘𝑢)))
309	265, 308	impbid 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
310	309	orbi1d 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
311	237, 310	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
312		orcom 401	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)))
313	311, 312	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢))))
314	313	ifbid 4141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
315		eqidd 2652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ∅ = ∅)
316	229, 314, 315	pm2.61ne 2908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
317	316	mpteq2dva 4777	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)))
318	317	fveq2d 6233	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))))
319		fvex 6239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑥) ∈ V
320	319, 181	ifex 4189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
322	321	ralrimivw 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
323	171	fnmpt 6058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
324	322, 323	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
325	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∅ ∈ V)
326		suppvalfn 7347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅})
327		nfcv 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝐵
328		nfcv 2793	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥𝐵
329		nffvmpt1 6237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)
330		nfcv 2793	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥∅
331	329, 330	nfne 2923	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅
332		nfv 1883	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅
333		fveq2 6229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥))
334	333	neeq1d 2882	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅))
335	327, 328, 331, 332, 334	cbvrab 3229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅}
336	326, 335	syl6eq 2701	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
337	324, 150, 325, 336	syl3anc 1366	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
338		eqidd 2652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
339	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
340	338, 339	fvmpt2d 6332	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
341	340	neeq1d 2882	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
342	339	biantrurd 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)))
343		dif1o 7625	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
344	342, 343	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)))
345	341, 344	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)))
346	345	rabbidva 3219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)})
347	337, 346	eqtrd 2685	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)})
348	320, 343	mpbiran 973	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)
349		ifeq1 4123	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
350	349, 185	syl6eq 2701	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
351	350	necon3i 2855	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → (𝐹‘𝑥) ≠ ∅)
352		iffalse 4128	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ⊆ (𝑂‘𝑢) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
353	352	necon1ai 2850	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂‘𝑢))
354	351, 353	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → ((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)))
355	265	expimpd 628	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
356	354, 355	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
357	348, 356	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜) → 𝑥 ∈ (𝑂‘suc 𝑢)))
358	357	3impia 1280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵 ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)) → 𝑥 ∈ (𝑂‘suc 𝑢))
359	358	rabssdv 3715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1𝑜)} ⊆ (𝑂‘suc 𝑢))
360	347, 359	eqsstrd 3672	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
361		eqeq1 2655	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
362		sseq1 3659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑦 ⊆ (𝑂‘𝑢)))
363	361, 362	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢))))
364		fveq2 6229	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
365	363, 364	ifbieq1d 4142	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
366	365	cbvmptv 4783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
367		fveq2 6229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑂‘suc 𝑢) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
368	367	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 = (𝑂‘suc 𝑢)) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
369	368	ifeq1da 4149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
370	362, 364	ifbieq1d 4142	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
371		fvex 6239	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑦) ∈ V
372	371, 181	ifex 4189	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅) ∈ V
373	370, 171, 372	fvmpt 6321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
374	373	ifeq2d 4138	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅)))
375		ifor 4168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
376	374, 375	syl6eqr 2703	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
377	369, 376	eqtr3d 2687	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
378	377	mpteq2ia 4773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
379	366, 378	eqtr4i 2676	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
380	8, 149, 150, 192, 210, 216, 360, 379	cantnfp1 8616	. . . . . . . . . . . . . . . . . . 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 2685	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
383	8, 9, 10, 2, 13, 113	cantnfsuc 8605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
384	198, 383	syldan 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
385	161	simp3d 1095	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
386	385	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
387	108	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) = 𝑋)
388	129	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ On)
389	137	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
390		onsssuc 5851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
391	388, 389, 390	syl2anc 694	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ⊆ 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢))
392	147, 391	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ suc 𝑢)
393	52	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (◡𝑂‘𝑋) ∈ dom 𝑂)
394		isorel 6616	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((◡𝑂‘𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
395	249, 393, 144, 394	syl12anc 1364	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
396	252	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((◡𝑂‘𝑋) E suc 𝑢 ↔ (◡𝑂‘𝑋) ∈ suc 𝑢)
397	254	epelc 5060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂‘(◡𝑂‘𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
398	395, 396, 397	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((◡𝑂‘𝑋) ∈ suc 𝑢 ↔ (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢)))
399	392, 398	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
400	387, 399	eqeltrrd 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
401		eleq2 2719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ (𝑂‘suc 𝑢)))
402		fveq2 6229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐹‘𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
403		fveq2 6229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐺‘𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
404	402, 403	eqeq12d 2666	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
405	401, 404	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
406	405	rspcv 3336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
407	210, 386, 400, 406	syl3c 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
408	407	oveq2d 6706	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))))
409	408	oveq1d 6705	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐺‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
410	384, 409	eqtr4d 2688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢)))
411	382, 410	eleq12d 2724	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑𝑜 (𝑂‘suc 𝑢)) ·𝑜 (𝐹‘(𝑂‘suc 𝑢))) +𝑜 (𝐻‘suc 𝑢))))
412	222, 411	bitr4d 271	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
413	412	biimpd 219	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
414	148, 413	embantd 59	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
415	414	expr 642	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
416	141, 415	sylbird 250	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
417		fveq2 6229	. . . . . . . . . . . . . . . . . . 19 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑂‘(◡𝑂‘𝑋)) = (𝑂‘suc 𝑢))
418	417	sseq2d 3666	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
419	418	ifbid 4141	. . . . . . . . . . . . . . . . 17 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
420	419	mpteq2dv 4778	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
421	420	fveq2d 6233	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
422		suceq 5828	. . . . . . . . . . . . . . . 16 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → suc (◡𝑂‘𝑋) = suc suc 𝑢)
423	422	fveq2d 6233	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (𝐻‘suc (◡𝑂‘𝑋)) = (𝐻‘suc suc 𝑢))
424	421, 423	eleq12d 2724	. . . . . . . . . . . . . 14 ⊢ ((◡𝑂‘𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
425	115, 424	syl5ibcom 235	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
426	425	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
427	426	a1dd 50	. . . . . . . . . . 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	135, 428	sylbid 230	. . . . . . . . 9 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
430	429	expimpd 628	. . . . . . . 8 ⊢ (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
431	430	com23 86	. . . . . . 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	82, 94, 106, 127, 432	finds2 7136	. . . . 5 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
434	70, 433	vtoclga 3303	. . . 4 ⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
435	57, 434	mpcom 38	. . 3 ⊢ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
436	44, 54, 435	mp2and 715	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))
437	156	feqmptd 6288	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)))
438		eqeq2 2662	. . . . . 6 ⊢ ((𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
439		eqeq2 2662	. . . . . 6 ⊢ (∅ = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
440		eqidd 2652	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = (𝐹‘𝑥))
441	207	ffvelrni 6398	. . . . . . . . . . . . . 14 ⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
442	44, 441	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
443	205, 442	sseldd 3637	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ 𝐵)
444		onelon 5786	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
445	10, 443, 444	syl2anc 694	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ On)
446	445	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
447		ontri1 5795	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
448	232, 446, 447	syl2anc 694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
449	448	con2bid 343	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
450		simprl 809	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ 𝐵)
451	385	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
452		eloni 5771	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂‘𝑋) ∈ On → Ord (◡𝑂‘𝑋))
453	129, 452	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ord (◡𝑂‘𝑋))
454		orduni 7036	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom 𝑂 → Ord ∪ dom 𝑂)
455	36, 454	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Ord ∪ dom 𝑂
456		ordtri1 5794	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord (◡𝑂‘𝑋) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
457	453, 455, 456	sylancl 695	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋)))
458	54, 457	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
459		isorel 6616	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
460	46, 44, 52, 459	syl12anc 1364	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋))))
461		fvex 6239	. . . . . . . . . . . . . . . . . 18 ⊢ (◡𝑂‘𝑋) ∈ V
462	461	epelc 5060	. . . . . . . . . . . . . . . . 17 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑋) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑋))
463		fvex 6239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂‘(◡𝑂‘𝑋)) ∈ V
464	463	epelc 5060	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)))
465	460, 462, 464	3bitr3g 302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋))))
466	108	eleq2d 2716	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
467	465, 466	bitrd 268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
468	458, 467	mtbid 313	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋)
469		onelon 5786	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On)
470	10, 162, 469	syl2anc 694	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ On)
471		ontri1 5795	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
472	470, 445, 471	syl2anc 694	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
473	468, 472	mpbird 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
474	473	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
475		simprr 811	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
476	470	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ On)
477	232	adantrr 753	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
478		ontr2 5810	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
479	476, 477, 478	syl2anc 694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
480	474, 475, 479	mp2and 715	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ 𝑥)
481		eleq2 2719	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥))
482		fveq2 6229	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
483		fveq2 6229	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥))
484	482, 483	eqeq12d 2666	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
485	481, 484	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
486	485	rspcv 3336	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
487	450, 451, 480, 486	syl3c 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥))
488	475	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
489	46	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
490	44	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ dom 𝑂)
491	51	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
492		ffvelrn 6397	. . . . . . . . . . . . . . . . . 18 ⊢ ((◡𝑂:(𝐺 supp ∅)⟶dom 𝑂 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
493	491, 492	sylancom 702	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ dom 𝑂)
494		isorel 6616	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (◡𝑂‘𝑥) ∈ dom 𝑂)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
495	489, 490, 493, 494	syl12anc 1364	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥))))
496	278	epelc 5060	. . . . . . . . . . . . . . . 16 ⊢ (∪ dom 𝑂 E (◡𝑂‘𝑥) ↔ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
497	280	epelc 5060	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)))
498	495, 496, 497	3bitr3g 302	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥))))
499	48	ad2antrr 762	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
500	499, 270	sylancom 702	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(◡𝑂‘𝑥)) = 𝑥)
501	500	eleq2d 2716	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
502	498, 501	bitrd 268	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
503	488, 502	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
504		elssuni 4499	. . . . . . . . . . . . . . 15 ⊢ ((◡𝑂‘𝑥) ∈ dom 𝑂 → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
505	493, 504	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
506	36, 493, 284	sylancr 696	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (◡𝑂‘𝑥) ∈ On)
507	506, 286	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (◡𝑂‘𝑥))
508		ordtri1 5794	. . . . . . . . . . . . . . 15 ⊢ ((Ord (◡𝑂‘𝑥) ∧ Ord ∪ dom 𝑂) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
509	507, 455, 508	sylancl 695	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥)))
510	505, 509	mpbid 222	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ ∪ dom 𝑂 ∈ (◡𝑂‘𝑥))
511	503, 510	pm2.65da 599	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
512	450, 511	eldifd 3618	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
513		ssid 3657	. . . . . . . . . . . . 13 ⊢ (𝐺 supp ∅) ⊆ (𝐺 supp ∅)
514	513	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
515	160, 514, 10, 182	suppssr 7371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑥) = ∅)
516	512, 515	syldan 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐺‘𝑥) = ∅)
517	487, 516	eqtrd 2685	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = ∅)
518	517	expr 642	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 → (𝐹‘𝑥) = ∅))
519	449, 518	sylbird 250	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂) → (𝐹‘𝑥) = ∅))
520	519	imp 444	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = ∅)
521	438, 439, 440, 520	ifbothda 4156	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
522	521	mpteq2dva 4777	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
523	437, 522	eqtrd 2685	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
524	523	fveq2d 6233	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
525	8, 9, 10, 2, 13, 113	cantnfval 8603	. . 3 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
526	43	fveq2d 6233	. . 3 ⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom 𝑂))
527	525, 526	eqtrd 2685	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc ∪ dom 𝑂))
528	436, 524, 527	3eltr4d 2745	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030   ≠ wne 2823  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∖ cdif 3604   ⊆ wss 3607  ∅c0 3948  ifcif 4119  ∪ cuni 4468   class class class wbr 4685  {copab 4745   ↦ cmpt 4762  Tr wtr 4785   E cep 5057   We wwe 5101  ^◡ccnv 5142  dom cdm 5143  Ord word 5760  Oncon0 5761  Lim wlim 5762  suc csuc 5763  Fun wfun 5920   Fn wfn 5921  ⟶wf 5922  –1-1-onto→wf1o 5925  ‘cfv 5926   Isom wiso 5927  (class class class)co 6690   ↦ cmpt2 6692  ωcom 7107   supp csupp 7340  seq_𝜔cseqom 7587  1_𝑜c1o 7598   +_𝑜 coa 7602   ·_𝑜 comu 7603   ↑_𝑜 coe 7604   ≈ cen 7994   finSupp cfsupp 8316  OrdIsocoi 8455   CNF ccnf 8596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-seqom 7588  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-oexp 7611  df-er 7787  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-oi 8456  df-cnf 8597

This theorem is referenced by:  cantnf  8628