cantnflem1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cantnflem1		Structured version Visualization version GIF version

Theorem cantnflem1 9136

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

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

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

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

Proof of Theorem cantnflem1 Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 7168	. . . . . 6 ⊢ (𝐺 supp ∅) ∈ V
2		cantnflem1.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
3	2	oion 8984	. . . . . 6 ⊢ ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
4	1, 3	mp1i 13	. . . . 5 ⊢ (𝜑 → dom 𝑂 ∈ On)
5		uniexg 7446	. . . . 5 ⊢ (dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V)
6		sucidg 6237	. . . . 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 9132	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
17		n0i 4249	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19		ovexd 7170	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 supp ∅) ∈ V)
20	8, 9, 10, 2, 13	cantnfcl 9114	. . . . . . . . . . 11 ⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
21	20	simpld 498	. . . . . . . . . 10 ⊢ (𝜑 → E We (𝐺 supp ∅))
22	2	oien 8986	. . . . . . . . . 10 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
23	19, 21, 22	syl2anc 587	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24		breq1 5033	. . . . . . . . . 10 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25		ensymb 8540	. . . . . . . . . . 11 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26		en0 8555	. . . . . . . . . . 11 ⊢ ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
27	25, 26	bitri 278	. . . . . . . . . 10 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
28	24, 27	syl6bb 290	. . . . . . . . 9 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
29	23, 28	syl5ibcom 248	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
30	18, 29	mtod 201	. . . . . . 7 ⊢ (𝜑 → ¬ dom 𝑂 = ∅)
31	20	simprd 499	. . . . . . . 8 ⊢ (𝜑 → dom 𝑂 ∈ ω)
32		nnlim 7573	. . . . . . . 8 ⊢ (dom 𝑂 ∈ ω → ¬ Lim dom 𝑂)
33	31, 32	syl 17	. . . . . . 7 ⊢ (𝜑 → ¬ Lim dom 𝑂)
34		ioran 981	. . . . . . 7 ⊢ (¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂) ↔ (¬ dom 𝑂 = ∅ ∧ ¬ Lim dom 𝑂))
35	30, 33, 34	sylanbrc 586	. . . . . 6 ⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
36	2	oicl 8977	. . . . . . 7 ⊢ Ord dom 𝑂
37		unizlim 6275	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
38	36, 37	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
39	35, 38	mtbird 328	. . . . 5 ⊢ (𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂)
40		orduniorsuc 7525	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
41	36, 40	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ∨ dom 𝑂 = suc ∪ dom 𝑂))
42	41	ord 861	. . . . 5 ⊢ (𝜑 → (¬ dom 𝑂 = ∪ dom 𝑂 → dom 𝑂 = suc ∪ dom 𝑂))
43	39, 42	mpd 15	. . . 4 ⊢ (𝜑 → dom 𝑂 = suc ∪ dom 𝑂)
44	7, 43	eleqtrrd 2893	. . 3 ⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂)
45	2	oiiso 8985	. . . . . . . 8 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
46	19, 21, 45	syl2anc 587	. . . . . . 7 ⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47		isof1o 7055	. . . . . . 7 ⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
48	46, 47	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
49		f1ocnv 6602	. . . . . 6 ⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ^◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50		f1of 6590	. . . . . 6 ⊢ (^◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂 → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
51	48, 49, 50	3syl 18	. . . . 5 ⊢ (𝜑 → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
52	51, 16	ffvelrnd 6829	. . . 4 ⊢ (𝜑 → (^◡𝑂‘𝑋) ∈ dom 𝑂)
53		elssuni 4830	. . . 4 ⊢ ((^◡𝑂‘𝑋) ∈ dom 𝑂 → (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . 3 ⊢ (𝜑 → (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
55	43, 31	eqeltrrd 2891	. . . . 5 ⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω)
56		peano2b 7576	. . . . 5 ⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω)
57	55, 56	sylibr 237	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ ω)
58		eleq1 2877	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂))
59		sseq2 3941	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂))
60	58, 59	anbi12d 633	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)))
61		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑂‘𝑦) = (𝑂‘∪ dom 𝑂))
62	61	sseq2d 3947	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
63	62	ifbid 4447	. . . . . . . . . 10 ⊢ (𝑦 = ∪ dom 𝑂 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
64	63	mpteq2dv 5126	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
65	64	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
66		suceq 6224	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂)
67	66	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc ∪ dom 𝑂))
68	65, 67	eleq12d 2884	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
69	60, 68	imbi12d 348	. . . . . 6 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
70	69	imbi2d 344	. . . . 5 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))))
71		eleq1 2877	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72		sseq2 3941	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ ∅))
73	71, 72	anbi12d 633	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅)))
74		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (𝑂‘𝑦) = (𝑂‘∅))
75	74	sseq2d 3947	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
76	75	ifbid 4447	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
77	76	mpteq2dv 5126	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
78	77	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
79		suceq 6224	. . . . . . . . 9 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
80	79	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
81	78, 80	eleq12d 2884	. . . . . . 7 ⊢ (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
82	73, 81	imbi12d 348	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83		eleq1 2877	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂))
84		sseq2 3941	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ 𝑢))
85	83, 84	anbi12d 633	. . . . . . 7 ⊢ (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)))
86		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑂‘𝑦) = (𝑂‘𝑢))
87	86	sseq2d 3947	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘𝑢)))
88	87	ifbid 4447	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
89	88	mpteq2dv 5126	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
90	89	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))
91		suceq 6224	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
92	91	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
93	90, 92	eleq12d 2884	. . . . . . 7 ⊢ (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
94	85, 93	imbi12d 348	. . . . . 6 ⊢ (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95		eleq1 2877	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96		sseq2 3941	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ suc 𝑢))
97	95, 96	anbi12d 633	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢)))
98		fveq2 6645	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑢 → (𝑂‘𝑦) = (𝑂‘suc 𝑢))
99	98	sseq2d 3947	. . . . . . . . . . 11 ⊢ (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
100	99	ifbid 4447	. . . . . . . . . 10 ⊢ (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
101	100	mpteq2dv 5126	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
102	101	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
103		suceq 6224	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104	103	fveq2d 6649	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105	102, 104	eleq12d 2884	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
106	97, 105	imbi12d 348	. . . . . 6 ⊢ (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107		f1ocnvfv2 7012	. . . . . . . . . . . . 13 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
108	48, 16, 107	syl2anc 587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
109	108	sseq2d 3947	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ 𝑋))
110	109	ifbid 4447	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))
111	110	mpteq2dv 5126	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)))
112	111	fveq2d 6649	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))))
113		cantnflem1.h	. . . . . . . . 9 ⊢ 𝐻 = seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑_o (𝑂‘𝑘)) ·_o (𝐺‘(𝑂‘𝑘))) +_o 𝑧)), ∅)
114	8, 9, 10, 11, 12, 13, 14, 15, 2, 113	cantnflem1d 9135	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)))
115	112, 114	eqeltrd 2890	. . . . . . 7 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)))
116		ss0 4306	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (^◡𝑂‘𝑋) = ∅)
117	116	fveq2d 6649	. . . . . . . . . . . . 13 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑂‘(^◡𝑂‘𝑋)) = (𝑂‘∅))
118	117	sseq2d 3947	. . . . . . . . . . . 12 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119	118	ifbid 4447	. . . . . . . . . . 11 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
120	119	mpteq2dv 5126	. . . . . . . . . 10 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
121	120	fveq2d 6649	. . . . . . . . 9 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
122		suceq 6224	. . . . . . . . . . 11 ⊢ ((^◡𝑂‘𝑋) = ∅ → suc (^◡𝑂‘𝑋) = suc ∅)
123	116, 122	syl 17	. . . . . . . . . 10 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → suc (^◡𝑂‘𝑋) = suc ∅)
124	123	fveq2d 6649	. . . . . . . . 9 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝐻‘suc (^◡𝑂‘𝑋)) = (𝐻‘suc ∅))
125	121, 124	eleq12d 2884	. . . . . . . 8 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126	125	adantl 485	. . . . . . 7 ⊢ ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127	115, 126	syl5ibcom 248	. . . . . 6 ⊢ (𝜑 → ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128		ordelon 6183	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ (^◡𝑂‘𝑋) ∈ dom 𝑂) → (^◡𝑂‘𝑋) ∈ On)
129	36, 52, 128	sylancr 590	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝑂‘𝑋) ∈ On)
130	36	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord dom 𝑂)
131		ordelon 6183	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
132	130, 131	sylan 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133		onsseleq 6200	. . . . . . . . . . 11 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((^◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (^◡𝑂‘𝑋) = suc 𝑢)))
134	129, 132, 133	syl2an2r 684	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((^◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (^◡𝑂‘𝑋) = suc 𝑢)))
135		sucelon 7512	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
136	132, 135	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
137		eloni 6169	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ On → Ord 𝑢)
138	136, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
139		ordsssuc 6245	. . . . . . . . . . . . 13 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ Ord 𝑢) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
140	129, 138, 139	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
141		ordtr 6173	. . . . . . . . . . . . . . . . 17 ⊢ (Ord dom 𝑂 → Tr dom 𝑂)
142	36, 141	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
143		simprl 770	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
144		trsuc 6243	. . . . . . . . . . . . . . . 16 ⊢ ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
145	142, 143, 144	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
146		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ⊆ 𝑢)
147	145, 146	jca 515	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢))
148	10	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
149		oecl 8145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑_o 𝐵) ∈ On)
150	9, 148, 149	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑_o 𝐵) ∈ On)
151	9	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
152	8, 151, 148	cantnff 9121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑_o 𝐵))
153	8, 9, 10	cantnfs 9113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
154	12, 153	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
155	154	simpld 498	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
156	155	ffvelrnda 6828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) ∈ 𝐴)
157	8, 9, 10	cantnfs 9113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)))
158	13, 157	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))
159	158	simpld 498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
160	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 9131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
161	160	simp1d 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
162	159, 161	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
163	162	ne0d 4251	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ≠ ∅)
164		on0eln0 6214	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
165	9, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
166	163, 165	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∅ ∈ 𝐴)
167	166	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∅ ∈ 𝐴)
168	156, 167	ifcld 4470	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ 𝐴)
169	168	fmpttd 6856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴)
170	10	mptexd 6964	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
171		funmpt 6362	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
173	154	simprd 499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 finSupp ∅)
174		ssidd 3938	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
175		0ex 5175	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ V
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∅ ∈ V)
177	155, 174, 10, 176	suppssr 7844	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑥) = ∅)
178	177	ifeq1d 4443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
179		ifid 4464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅) = ∅
180	178, 179	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
181	180, 10	suppss2 7847	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
182		fsuppsssupp 8833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V ∧ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
183	170, 172, 173, 181, 182	syl22anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
184	8, 9, 10	cantnfs 9113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)))
185	169, 183, 184	mpbir2and 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
186	185	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
187	152, 186	ffvelrnd 6829	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑_o 𝐵))
188		onelon 6184	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑_o 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑_o 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
189	150, 187, 188	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
190	31	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
191		elnn 7570	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
192	143, 190, 191	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
193	113	cantnfvalf 9112	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻:ω⟶On
194	193	ffvelrni 6827	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
195	192, 194	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
196		suppssdm 7826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 supp ∅) ⊆ dom 𝐺
197	196, 159	fssdm 6504	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
198	197	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
199	2	oif 8978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅)
200	199	ffvelrni 6827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
201	143, 200	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
202	198, 201	sseldd 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
203		onelon 6184	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
204	10, 202, 203	syl2an2r 684	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
205		oecl 8145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On)
206	9, 204, 205	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On)
207	155	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐹:𝐵⟶𝐴)
208	207, 202	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
209		onelon 6184	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
210	9, 208, 209	syl2an2r 684	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
211		omcl 8144	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
212	206, 210, 211	syl2anc 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
213		oaord 8156	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On ∧ (𝐻‘suc 𝑢) ∈ On ∧ ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) ∈ On) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢))))
214	189, 195, 212, 213	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢))))
215		ifeq1 4429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
216		ifid 4464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
217	215, 216	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = ∅)
218		ifeq1 4429	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅))
219		ifid 4464	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅) = ∅
220	218, 219	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = ∅)
221	217, 220	eqeq12d 2814	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) ↔ ∅ = ∅))
222		onss 7485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
223	10, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ⊆ On)
224	223	sselda 3915	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
225	224	adantlr 714	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
226	204	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
227		onsseleq 6200	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
228	225, 226, 227	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
229	228	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
230	199	ffvelrni 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
231	145, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
232	198, 231	sseldd 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵)
233		onelon 6184	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On)
234	10, 232, 233	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On)
235	234	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑂‘𝑢) ∈ On)
236		onsssuc 6246	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
237	225, 235, 236	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
238		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑢 ∈ V
239	238	sucid 6238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ suc 𝑢
240	46	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
241		isorel 7058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
242	240, 145, 143, 241	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
243	238	sucex 7506	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ suc 𝑢 ∈ V
244	243	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢)
245		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑂‘suc 𝑢) ∈ V
246	245	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
247	242, 244, 246	3bitr3g 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢)))
248	239, 247	mpbii 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
249		eloni 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
250	204, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
251		ordelsuc 7515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑂‘𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
252	234, 250, 251	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
253	248, 252	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
254	253	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
255	254	sseld 3914	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
256	237, 255	sylbid 243	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
257		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥)
258	240	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
259	258, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
260	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 9134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
261		f1ocnvfv2 7012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
262	259, 260, 261	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
263	257, 262	eleqtrrd 2893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥)))
264	145	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
265	259, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
266	265, 260	ffvelrnd 6829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
267		isorel 7058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂)) → (𝑢 E (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥))))
268	258, 264, 266, 267	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 E (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥))))
269		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (^◡𝑂‘𝑥) ∈ V
270	269	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 E (^◡𝑂‘𝑥) ↔ 𝑢 ∈ (^◡𝑂‘𝑥))
271		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑂‘(^◡𝑂‘𝑥)) ∈ V
272	271	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥)))
273	268, 270, 272	3bitr3g 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥))))
274	263, 273	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ (^◡𝑂‘𝑥))
275		ordelon 6183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((Ord dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂) → (^◡𝑂‘𝑥) ∈ On)
276	36, 266, 275	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (^◡𝑂‘𝑥) ∈ On)
277		eloni 6169	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((^◡𝑂‘𝑥) ∈ On → Ord (^◡𝑂‘𝑥))
278	276, 277	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → Ord (^◡𝑂‘𝑥))
279		ordelsuc 7515	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ (^◡𝑂‘𝑥) ∧ Ord (^◡𝑂‘𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (^◡𝑂‘𝑥)))
280	274, 278, 279	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (^◡𝑂‘𝑥)))
281	274, 280	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (^◡𝑂‘𝑥))
282	143	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
283	36, 282, 131	sylancr 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
284		ontri1 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((suc 𝑢 ∈ On ∧ (^◡𝑂‘𝑥) ∈ On) → (suc 𝑢 ⊆ (^◡𝑂‘𝑥) ↔ ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢))
285	283, 276, 284	syl2anc 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (^◡𝑂‘𝑥) ↔ ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢))
286	281, 285	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢)
287		isorel 7058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((^◡𝑂‘𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
288	258, 266, 282, 287	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
289	243	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (^◡𝑂‘𝑥) ∈ suc 𝑢)
290	245	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢))
291	288, 289, 290	3bitr3g 316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) ∈ suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢)))
292	262	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
293	291, 292	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) ∈ suc 𝑢 ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
294	286, 293	mtbid 327	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
295	294	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑂‘𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
296	295	con2d 136	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂‘𝑢) ∈ 𝑥))
297		ontri1 6193	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
298	225, 235, 297	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
299	296, 298	sylibrd 262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂‘𝑢)))
300	256, 299	impbid 215	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
301	300	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
302	229, 301	bitr4d 285	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
303		orcom 867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)))
304	302, 303	syl6bb 290	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢))))
305	304	ifbid 4447	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
306		eqidd 2799	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ∅ = ∅)
307	221, 305, 306	pm2.61ne 3072	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
308	307	mpteq2dva 5125	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)))
309	308	fveq2d 6649	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))))
310		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑥) ∈ V
311	310, 175	ifex 4473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V
312	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
313	312	ralrimivw 3150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
314		eqid 2798	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
315	314	fnmpt 6460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
316	313, 315	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵)
317	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ∅ ∈ V)
318		suppvalfn 7820	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅})
319		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝐵
320		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥𝐵
321		nffvmpt1 6656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)
322		nfcv 2955	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥∅
323	321, 322	nfne 3087	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅
324		nfv 1915	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅
325		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥))
326	325	neeq1d 3046	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅))
327	319, 320, 323, 324, 326	cbvrabw 3437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅}
328	318, 327	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
329	316, 148, 317, 328	syl3anc 1368	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
330		eqidd 2799	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
331	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
332	330, 331	fvmpt2d 6758	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
333	332	neeq1d 3046	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
334	331	biantrurd 536	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)))
335		dif1o 8108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
336	334, 335	syl6bbr 292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)))
337	333, 336	bitrd 282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)))
338	337	rabbidva 3425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)})
339	329, 338	eqtrd 2833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)})
340	311, 335	mpbiran 708	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)
341		ifeq1 4429	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
342	341, 179	eqtrdi 2849	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
343	342	necon3i 3019	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → (𝐹‘𝑥) ≠ ∅)
344		iffalse 4434	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ⊆ (𝑂‘𝑢) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
345	344	necon1ai 3014	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂‘𝑢))
346	343, 345	jca 515	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → ((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)))
347	256	expimpd 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
348	346, 347	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
349	340, 348	syl5bi 245	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) → 𝑥 ∈ (𝑂‘suc 𝑢)))
350	349	3impia 1114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵 ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)) → 𝑥 ∈ (𝑂‘suc 𝑢))
351	350	rabssdv 4002	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)} ⊆ (𝑂‘suc 𝑢))
352	339, 351	eqsstrd 3953	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
353		eqeq1 2802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
354		sseq1 3940	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑦 ⊆ (𝑂‘𝑢)))
355	353, 354	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢))))
356		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
357	355, 356	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
358	357	cbvmptv 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
359		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑂‘suc 𝑢) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
360	359	adantl 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 = (𝑂‘suc 𝑢)) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
361	360	ifeq1da 4455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
362	354, 356	ifbieq1d 4448	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
363		fvex 6658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑦) ∈ V
364	363, 175	ifex 4473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅) ∈ V
365	362, 314, 364	fvmpt 6745	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
366	365	ifeq2d 4444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅)))
367		ifor 4477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
368	366, 367	eqtr4di 2851	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
369	361, 368	eqtr3d 2835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
370	369	mpteq2ia 5121	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
371	358, 370	eqtr4i 2824	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
372	8, 151, 148, 186, 202, 208, 352, 371	cantnfp1 9128	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))))
373	372	simprd 499	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
374	309, 373	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
375	8, 9, 10, 2, 13, 113	cantnfsuc 9117	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
376	192, 375	syldan 594	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
377	160	simp3d 1141	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
378	377	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
379	108	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
380	136	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
381		onsssuc 6246	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
382	129, 380, 381	syl2an2r 684	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
383	146, 382	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ∈ suc 𝑢)
384	52	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ∈ dom 𝑂)
385		isorel 7058	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((^◡𝑂‘𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
386	240, 384, 143, 385	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
387	243	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢)
388	245	epeli 5432	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
389	386, 387, 388	3bitr3g 316	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) ∈ suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢)))
390	383, 389	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
391	379, 390	eqeltrrd 2891	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
392		eleq2 2878	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ (𝑂‘suc 𝑢)))
393		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐹‘𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
394		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐺‘𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
395	393, 394	eqeq12d 2814	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
396	392, 395	imbi12d 348	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
397	396	rspcv 3566	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
398	202, 378, 391, 397	syl3c 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
399	398	oveq2d 7151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))))
400	399	oveq1d 7150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
401	376, 400	eqtr4d 2836	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
402	374, 401	eleq12d 2884	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢) ↔ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢))))
403	214, 402	bitr4d 285	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
404	403	biimpd 232	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
405	147, 404	embantd 59	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
406	405	expr 460	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
407	140, 406	sylbird 263	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
408		fveq2 6645	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑂‘(^◡𝑂‘𝑋)) = (𝑂‘suc 𝑢))
409	408	sseq2d 3947	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
410	409	ifbid 4447	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
411	410	mpteq2dv 5126	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
412	411	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
413		suceq 6224	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → suc (^◡𝑂‘𝑋) = suc suc 𝑢)
414	413	fveq2d 6649	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝐻‘suc (^◡𝑂‘𝑋)) = (𝐻‘suc suc 𝑢))
415	412, 414	eleq12d 2884	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
416	115, 415	syl5ibcom 248	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
417	416	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
418	417	a1dd 50	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) = suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
419	407, 418	jaod 856	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → (((^◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (^◡𝑂‘𝑋) = suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
420	134, 419	sylbid 243	. . . . . . . . 9 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
421	420	expimpd 457	. . . . . . . 8 ⊢ (𝜑 → ((suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢) → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
422	421	com23 86	. . . . . . 7 ⊢ (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
423	422	a1i 11	. . . . . 6 ⊢ (𝑢 ∈ ω → (𝜑 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))))
424	82, 94, 106, 127, 423	finds2 7591	. . . . 5 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
425	70, 424	vtoclga 3522	. . . 4 ⊢ (∪ dom 𝑂 ∈ ω → (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
426	57, 425	mpcom 38	. . 3 ⊢ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
427	44, 54, 426	mp2and 698	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))
428	155	feqmptd 6708	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)))
429		eqeq2 2810	. . . . . 6 ⊢ ((𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
430		eqeq2 2810	. . . . . 6 ⊢ (∅ = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
431		eqidd 2799	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = (𝐹‘𝑥))
432	199	ffvelrni 6827	. . . . . . . . . . . . . 14 ⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
433	44, 432	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
434	197, 433	sseldd 3916	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ 𝐵)
435		onelon 6184	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
436	10, 434, 435	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ On)
437	436	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
438		ontri1 6193	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
439	224, 437, 438	syl2anc 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
440	439	con2bid 358	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
441		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ 𝐵)
442	377	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
443		eloni 6169	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂‘𝑋) ∈ On → Ord (^◡𝑂‘𝑋))
444	129, 443	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ord (^◡𝑂‘𝑋))
445		orduni 7489	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom 𝑂 → Ord ∪ dom 𝑂)
446	36, 445	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Ord ∪ dom 𝑂
447		ordtri1 6192	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord (^◡𝑂‘𝑋) ∧ Ord ∪ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋)))
448	444, 446, 447	sylancl 589	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋)))
449	54, 448	mpbid 235	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋))
450		isorel 7058	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋))))
451	46, 44, 52, 450	syl12anc 835	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋))))
452		fvex 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑂‘𝑋) ∈ V
453	452	epeli 5432	. . . . . . . . . . . . . . . . 17 ⊢ (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋))
454		fvex 6658	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂‘(^◡𝑂‘𝑋)) ∈ V
455	454	epeli 5432	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋)))
456	451, 453, 455	3bitr3g 316	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋))))
457	108	eleq2d 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
458	456, 457	bitrd 282	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
459	449, 458	mtbid 327	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋)
460		onelon 6184	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On)
461	10, 161, 460	syl2anc 587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ On)
462		ontri1 6193	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
463	461, 436, 462	syl2anc 587	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
464	459, 463	mpbird 260	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
465	464	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
466		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
467	224	adantrr 716	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
468		ontr2 6206	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
469	461, 467, 468	syl2an2r 684	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
470	465, 466, 469	mp2and 698	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ 𝑥)
471		eleq2 2878	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥))
472		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
473		fveq2 6645	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥))
474	472, 473	eqeq12d 2814	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
475	471, 474	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
476	475	rspcv 3566	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
477	441, 442, 470, 476	syl3c 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥))
478	466	adantr 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
479	46	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
480	44	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ dom 𝑂)
481	51	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
482		ffvelrn 6826	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
483	481, 482	sylancom 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
484		isorel 7058	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂)) → (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥))))
485	479, 480, 483, 484	syl12anc 835	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥))))
486	269	epeli 5432	. . . . . . . . . . . . . . . 16 ⊢ (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
487	271	epeli 5432	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥)))
488	485, 486, 487	3bitr3g 316	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥))))
489	48	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
490	489, 261	sylancom 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
491	490	eleq2d 2875	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
492	488, 491	bitrd 282	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
493	478, 492	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
494		elssuni 4830	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑥) ∈ dom 𝑂 → (^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
495	483, 494	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
496	36, 483, 275	sylancr 590	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ On)
497	496, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (^◡𝑂‘𝑥))
498		ordtri1 6192	. . . . . . . . . . . . . . 15 ⊢ ((Ord (^◡𝑂‘𝑥) ∧ Ord ∪ dom 𝑂) → ((^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥)))
499	497, 446, 498	sylancl 589	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥)))
500	495, 499	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
501	493, 500	pm2.65da 816	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
502	441, 501	eldifd 3892	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
503		ssidd 3938	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
504	159, 503, 10, 176	suppssr 7844	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑥) = ∅)
505	502, 504	syldan 594	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐺‘𝑥) = ∅)
506	477, 505	eqtrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = ∅)
507	506	expr 460	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 → (𝐹‘𝑥) = ∅))
508	440, 507	sylbird 263	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂) → (𝐹‘𝑥) = ∅))
509	508	imp 410	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = ∅)
510	429, 430, 431, 509	ifbothda 4462	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
511	510	mpteq2dva 5125	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
512	428, 511	eqtrd 2833	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
513	512	fveq2d 6649	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
514	8, 9, 10, 2, 13, 113	cantnfval 9115	. . 3 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
515	43	fveq2d 6649	. . 3 ⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom 𝑂))
516	514, 515	eqtrd 2833	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc ∪ dom 𝑂))
517	427, 513, 516	3eltr4d 2905	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2987 ∀wral 3106 ∃wrex 3107 {crab 3110 Vcvv 3441 ∖ cdif 3878 ⊆ wss 3881 ∅c0 4243 ifcif 4425 ∪ cuni 4800 class class class wbr 5030 {copab 5092 ↦ cmpt 5110 Tr wtr 5136 E cep 5429 We wwe 5477 ^◡ccnv 5518 dom cdm 5519 Ord word 6158 Oncon0 6159 Lim wlim 6160 suc csuc 6161 Fun wfun 6318 Fn wfn 6319 ⟶wf 6320 –1-1-onto→wf1o 6323 ‘cfv 6324 Isom wiso 6325 (class class class)co 7135 ∈ cmpo 7137 ωcom 7560 supp csupp 7813 seq_ωcseqom 8066 1_oc1o 8078 +_o coa 8082 ·_o comu 8083 ↑_o coe 8084 ≈ cen 8489 finSupp cfsupp 8817 OrdIsocoi 8957 CNF ccnf 9108

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-seqom 8067 df-1o 8085 df-2o 8086 df-oadd 8089 df-omul 8090 df-oexp 8091 df-er 8272 df-map 8391 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-oi 8958 df-cnf 9109

This theorem is referenced by: cantnf 9140

W3C validator