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 9447

Description: Lemma for cantnf 9451. 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 7308	. . . . . 6 ⊢ (𝐺 supp ∅) ∈ V
2		cantnflem1.o	. . . . . . 7 ⊢ 𝑂 = OrdIso( E , (𝐺 supp ∅))
3	2	oion 9295	. . . . . 6 ⊢ ((𝐺 supp ∅) ∈ V → dom 𝑂 ∈ On)
4	1, 3	mp1i 13	. . . . 5 ⊢ (𝜑 → dom 𝑂 ∈ On)
5		uniexg 7593	. . . . 5 ⊢ (dom 𝑂 ∈ On → ∪ dom 𝑂 ∈ V)
6		sucidg 6344	. . . . 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 9443	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (𝐺 supp ∅))
17		n0i 4267	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝐺 supp ∅) → ¬ (𝐺 supp ∅) = ∅)
18	16, 17	syl 17	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝐺 supp ∅) = ∅)
19		ovexd 7310	. . . . . . . . . 10 ⊢ (𝜑 → (𝐺 supp ∅) ∈ V)
20	8, 9, 10, 2, 13	cantnfcl 9425	. . . . . . . . . . 11 ⊢ (𝜑 → ( E We (𝐺 supp ∅) ∧ dom 𝑂 ∈ ω))
21	20	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → E We (𝐺 supp ∅))
22	2	oien 9297	. . . . . . . . . 10 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → dom 𝑂 ≈ (𝐺 supp ∅))
23	19, 21, 22	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → dom 𝑂 ≈ (𝐺 supp ∅))
24		breq1 5077	. . . . . . . . . 10 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ ∅ ≈ (𝐺 supp ∅)))
25		ensymb 8788	. . . . . . . . . . 11 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) ≈ ∅)
26		en0 8803	. . . . . . . . . . 11 ⊢ ((𝐺 supp ∅) ≈ ∅ ↔ (𝐺 supp ∅) = ∅)
27	25, 26	bitri 274	. . . . . . . . . 10 ⊢ (∅ ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅)
28	24, 27	bitrdi 287	. . . . . . . . 9 ⊢ (dom 𝑂 = ∅ → (dom 𝑂 ≈ (𝐺 supp ∅) ↔ (𝐺 supp ∅) = ∅))
29	23, 28	syl5ibcom 244	. . . . . . . 8 ⊢ (𝜑 → (dom 𝑂 = ∅ → (𝐺 supp ∅) = ∅))
30	18, 29	mtod 197	. . . . . . 7 ⊢ (𝜑 → ¬ dom 𝑂 = ∅)
31	20	simprd 496	. . . . . . . 8 ⊢ (𝜑 → dom 𝑂 ∈ ω)
32		nnlim 7726	. . . . . . . 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 583	. . . . . 6 ⊢ (𝜑 → ¬ (dom 𝑂 = ∅ ∨ Lim dom 𝑂))
36	2	oicl 9288	. . . . . . 7 ⊢ Ord dom 𝑂
37		unizlim 6383	. . . . . . 7 ⊢ (Ord dom 𝑂 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
38	36, 37	mp1i 13	. . . . . 6 ⊢ (𝜑 → (dom 𝑂 = ∪ dom 𝑂 ↔ (dom 𝑂 = ∅ ∨ Lim dom 𝑂)))
39	35, 38	mtbird 325	. . . . 5 ⊢ (𝜑 → ¬ dom 𝑂 = ∪ dom 𝑂)
40		orduniorsuc 7677	. . . . . . 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 2842	. . 3 ⊢ (𝜑 → ∪ dom 𝑂 ∈ dom 𝑂)
45	2	oiiso 9296	. . . . . . . 8 ⊢ (((𝐺 supp ∅) ∈ V ∧ E We (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
46	19, 21, 45	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
47		isof1o 7194	. . . . . . 7 ⊢ (𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
48	46, 47	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
49		f1ocnv 6728	. . . . . 6 ⊢ (𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) → ^◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂)
50		f1of 6716	. . . . . 6 ⊢ (^◡𝑂:(𝐺 supp ∅)–1-1-onto→dom 𝑂 → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
51	48, 49, 50	3syl 18	. . . . 5 ⊢ (𝜑 → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
52	51, 16	ffvelrnd 6962	. . . 4 ⊢ (𝜑 → (^◡𝑂‘𝑋) ∈ dom 𝑂)
53		elssuni 4871	. . . 4 ⊢ ((^◡𝑂‘𝑋) ∈ dom 𝑂 → (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
54	52, 53	syl 17	. . 3 ⊢ (𝜑 → (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)
55	43, 31	eqeltrrd 2840	. . . . 5 ⊢ (𝜑 → suc ∪ dom 𝑂 ∈ ω)
56		peano2b 7729	. . . . 5 ⊢ (∪ dom 𝑂 ∈ ω ↔ suc ∪ dom 𝑂 ∈ ω)
57	55, 56	sylibr 233	. . . 4 ⊢ (𝜑 → ∪ dom 𝑂 ∈ ω)
58		eleq1 2826	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑦 ∈ dom 𝑂 ↔ ∪ dom 𝑂 ∈ dom 𝑂))
59		sseq2 3947	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂))
60	58, 59	anbi12d 631	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂)))
61		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑂‘𝑦) = (𝑂‘∪ dom 𝑂))
62	61	sseq2d 3953	. . . . . . . . . . 11 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
63	62	ifbid 4482	. . . . . . . . . 10 ⊢ (𝑦 = ∪ dom 𝑂 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
64	63	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
65	64	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
66		suceq 6331	. . . . . . . . 9 ⊢ (𝑦 = ∪ dom 𝑂 → suc 𝑦 = suc ∪ dom 𝑂)
67	66	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = ∪ dom 𝑂 → (𝐻‘suc 𝑦) = (𝐻‘suc ∪ dom 𝑂))
68	65, 67	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))
69	60, 68	imbi12d 345	. . . . . 6 ⊢ (𝑦 = ∪ dom 𝑂 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))))
70	69	imbi2d 341	. . . . 5 ⊢ (𝑦 = ∪ dom 𝑂 → ((𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))) ↔ (𝜑 → ((∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂)))))
71		eleq1 2826	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝑦 ∈ dom 𝑂 ↔ ∅ ∈ dom 𝑂))
72		sseq2 3947	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ ∅))
73	71, 72	anbi12d 631	. . . . . . 7 ⊢ (𝑦 = ∅ → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅)))
74		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → (𝑂‘𝑦) = (𝑂‘∅))
75	74	sseq2d 3953	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘∅)))
76	75	ifbid 4482	. . . . . . . . . 10 ⊢ (𝑦 = ∅ → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
77	76	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑦 = ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
78	77	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
79		suceq 6331	. . . . . . . . 9 ⊢ (𝑦 = ∅ → suc 𝑦 = suc ∅)
80	79	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = ∅ → (𝐻‘suc 𝑦) = (𝐻‘suc ∅))
81	78, 80	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
82	73, 81	imbi12d 345	. . . . . 6 ⊢ (𝑦 = ∅ → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅))))
83		eleq1 2826	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝑦 ∈ dom 𝑂 ↔ 𝑢 ∈ dom 𝑂))
84		sseq2 3947	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ 𝑢))
85	83, 84	anbi12d 631	. . . . . . 7 ⊢ (𝑦 = 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)))
86		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑢 → (𝑂‘𝑦) = (𝑂‘𝑢))
87	86	sseq2d 3953	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘𝑢)))
88	87	ifbid 4482	. . . . . . . . . 10 ⊢ (𝑦 = 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
89	88	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
90	89	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))
91		suceq 6331	. . . . . . . . 9 ⊢ (𝑦 = 𝑢 → suc 𝑦 = suc 𝑢)
92	91	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc 𝑢))
93	90, 92	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)))
94	85, 93	imbi12d 345	. . . . . 6 ⊢ (𝑦 = 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢))))
95		eleq1 2826	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝑦 ∈ dom 𝑂 ↔ suc 𝑢 ∈ dom 𝑂))
96		sseq2 3947	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((^◡𝑂‘𝑋) ⊆ 𝑦 ↔ (^◡𝑂‘𝑋) ⊆ suc 𝑢))
97	95, 96	anbi12d 631	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) ↔ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢)))
98		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑦 = suc 𝑢 → (𝑂‘𝑦) = (𝑂‘suc 𝑢))
99	98	sseq2d 3953	. . . . . . . . . . 11 ⊢ (𝑦 = suc 𝑢 → (𝑥 ⊆ (𝑂‘𝑦) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
100	99	ifbid 4482	. . . . . . . . . 10 ⊢ (𝑦 = suc 𝑢 → if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
101	100	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
102	101	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
103		suceq 6331	. . . . . . . . 9 ⊢ (𝑦 = suc 𝑢 → suc 𝑦 = suc suc 𝑢)
104	103	fveq2d 6778	. . . . . . . 8 ⊢ (𝑦 = suc 𝑢 → (𝐻‘suc 𝑦) = (𝐻‘suc suc 𝑢))
105	102, 104	eleq12d 2833	. . . . . . 7 ⊢ (𝑦 = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
106	97, 105	imbi12d 345	. . . . . 6 ⊢ (𝑦 = suc 𝑢 → (((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦)) ↔ ((suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
107		f1ocnvfv2 7149	. . . . . . . . . . . . 13 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑋 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
108	48, 16, 107	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
109	108	sseq2d 3953	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ 𝑋))
110	109	ifbid 4482	. . . . . . . . . 10 ⊢ (𝜑 → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))
111	110	mpteq2dv 5176	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅)))
112	111	fveq2d 6778	. . . . . . . 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 9446	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ 𝑋, (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)))
115	112, 114	eqeltrd 2839	. . . . . . 7 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)))
116		ss0 4332	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (^◡𝑂‘𝑋) = ∅)
117	116	fveq2d 6778	. . . . . . . . . . . . 13 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑂‘(^◡𝑂‘𝑋)) = (𝑂‘∅))
118	117	sseq2d 3953	. . . . . . . . . . . 12 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘∅)))
119	118	ifbid 4482	. . . . . . . . . . 11 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))
120	119	mpteq2dv 5176	. . . . . . . . . 10 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅)))
121	120	fveq2d 6778	. . . . . . . . 9 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))))
122		suceq 6331	. . . . . . . . . . 11 ⊢ ((^◡𝑂‘𝑋) = ∅ → suc (^◡𝑂‘𝑋) = suc ∅)
123	116, 122	syl 17	. . . . . . . . . 10 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → suc (^◡𝑂‘𝑋) = suc ∅)
124	123	fveq2d 6778	. . . . . . . . 9 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (𝐻‘suc (^◡𝑂‘𝑋)) = (𝐻‘suc ∅))
125	121, 124	eleq12d 2833	. . . . . . . 8 ⊢ ((^◡𝑂‘𝑋) ⊆ ∅ → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
126	125	adantl 482	. . . . . . 7 ⊢ ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
127	115, 126	syl5ibcom 244	. . . . . 6 ⊢ (𝜑 → ((∅ ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ ∅) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∅), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∅)))
128		ordelon 6290	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ (^◡𝑂‘𝑋) ∈ dom 𝑂) → (^◡𝑂‘𝑋) ∈ On)
129	36, 52, 128	sylancr 587	. . . . . . . . . . 11 ⊢ (𝜑 → (^◡𝑂‘𝑋) ∈ On)
130	36	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord dom 𝑂)
131		ordelon 6290	. . . . . . . . . . . 12 ⊢ ((Ord dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
132	130, 131	sylan 580	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → suc 𝑢 ∈ On)
133		onsseleq 6307	. . . . . . . . . . 11 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ suc 𝑢 ∈ On) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((^◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (^◡𝑂‘𝑋) = suc 𝑢)))
134	129, 132, 133	syl2an2r 682	. . . . . . . . . 10 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 ↔ ((^◡𝑂‘𝑋) ∈ suc 𝑢 ∨ (^◡𝑂‘𝑋) = suc 𝑢)))
135		sucelon 7664	. . . . . . . . . . . . . . 15 ⊢ (𝑢 ∈ On ↔ suc 𝑢 ∈ On)
136	132, 135	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ On)
137		eloni 6276	. . . . . . . . . . . . . 14 ⊢ (𝑢 ∈ On → Ord 𝑢)
138	136, 137	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → Ord 𝑢)
139		ordsssuc 6352	. . . . . . . . . . . . 13 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ Ord 𝑢) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
140	129, 138, 139	syl2an2r 682	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
141		ordtr 6280	. . . . . . . . . . . . . . . . 17 ⊢ (Ord dom 𝑂 → Tr dom 𝑂)
142	36, 141	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → Tr dom 𝑂)
143		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ dom 𝑂)
144		trsuc 6350	. . . . . . . . . . . . . . . 16 ⊢ ((Tr dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂) → 𝑢 ∈ dom 𝑂)
145	142, 143, 144	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ dom 𝑂)
146		simprr 770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ⊆ 𝑢)
147	145, 146	jca 512	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢))
148	10	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐵 ∈ On)
149		oecl 8367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑_o 𝐵) ∈ On)
150	9, 148, 149	syl2an2r 682	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑_o 𝐵) ∈ On)
151	9	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐴 ∈ On)
152	8, 151, 148	cantnff 9432	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑_o 𝐵))
153	8, 9, 10	cantnfs 9424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
154	12, 153	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))
155	154	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝐹:𝐵⟶𝐴)
156	155	ffvelrnda 6961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) ∈ 𝐴)
157	8, 9, 10	cantnfs 9424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)))
158	13, 157	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))
159	158	simpld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
160	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 9442	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))
161	160	simp1d 1141	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
162	159, 161	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐺‘𝑋) ∈ 𝐴)
163	162	ne0d 4269	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 ≠ ∅)
164		on0eln0 6321	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐴 ∈ On → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
165	9, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅))
166	163, 165	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → ∅ ∈ 𝐴)
167	166	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∅ ∈ 𝐴)
168	156, 167	ifcld 4505	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ 𝐴)
169	168	fmpttd 6989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴)
170	10	mptexd 7100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V)
171		funmpt 6472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
173	154	simprd 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 finSupp ∅)
174		ssidd 3944	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → (𝐹 supp ∅) ⊆ (𝐹 supp ∅))
175		0ex 5231	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∅ ∈ V
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → ∅ ∈ V)
177	155, 174, 10, 176	suppssr 8012	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → (𝐹‘𝑥) = ∅)
178	177	ifeq1d 4478	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
179		ifid 4499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅) = ∅
180	178, 179	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐹 supp ∅))) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
181	180, 10	suppss2 8016	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))
182		fsuppsssupp 9144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ V ∧ Fun (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∧ (𝐹 finSupp ∅ ∧ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝐹 supp ∅))) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
183	170, 172, 173, 181, 182	syl22anc 836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)
184	8, 9, 10	cantnfs 9424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆 ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)):𝐵⟶𝐴 ∧ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) finSupp ∅)))
185	169, 183, 184	mpbir2and 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
186	185	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) ∈ 𝑆)
187	152, 186	ffvelrnd 6962	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑_o 𝐵))
188		onelon 6291	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑_o 𝐵) ∈ On ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐴 ↑_o 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
189	150, 187, 188	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ On)
190	31	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → dom 𝑂 ∈ ω)
191		elnn 7723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((suc 𝑢 ∈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → suc 𝑢 ∈ ω)
192	143, 190, 191	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc 𝑢 ∈ ω)
193	113	cantnfvalf 9423	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐻:ω⟶On
194	193	ffvelrni 6960	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑢 ∈ ω → (𝐻‘suc 𝑢) ∈ On)
195	192, 194	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc 𝑢) ∈ On)
196		suppssdm 7993	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 supp ∅) ⊆ dom 𝐺
197	196, 159	fssdm 6620	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ 𝐵)
198	197	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐺 supp ∅) ⊆ 𝐵)
199	2	oif 9289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑂:dom 𝑂⟶(𝐺 supp ∅)
200	199	ffvelrni 6960	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (suc 𝑢 ∈ dom 𝑂 → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
201	143, 200	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ (𝐺 supp ∅))
202	198, 201	sseldd 3922	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ 𝐵)
203		onelon 6291	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐵 ∈ On ∧ (𝑂‘suc 𝑢) ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
204	10, 202, 203	syl2an2r 682	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘suc 𝑢) ∈ On)
205		oecl 8367	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On)
206	9, 204, 205	syl2an2r 682	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On)
207	155	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝐹:𝐵⟶𝐴)
208	207, 202	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴)
209		onelon 6291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ 𝐴) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
210	9, 208, 209	syl2an2r 682	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) ∈ On)
211		omcl 8366	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ∈ On ∧ (𝐹‘(𝑂‘suc 𝑢)) ∈ On) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
212	206, 210, 211	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) ∈ On)
213		oaord 8378	. . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))) ∈ (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢))))
215		ifeq1 4463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅))
216		ifid 4499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if(𝑥 ⊆ (𝑂‘suc 𝑢), ∅, ∅) = ∅
217	215, 216	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = ∅)
218		ifeq1 4463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅))
219		ifid 4499	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), ∅, ∅) = ∅
220	218, 219	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹‘𝑥) = ∅ → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = ∅)
221	217, 220	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹‘𝑥) = ∅ → (if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) ↔ ∅ = ∅))
222		onss 7634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝐵 ∈ On → 𝐵 ⊆ On)
223	10, 222	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → 𝐵 ⊆ On)
224	223	sselda 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
225	224	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On)
226	204	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑂‘suc 𝑢) ∈ On)
227		onsseleq 6307	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑥 ∈ On ∧ (𝑂‘suc 𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
228	225, 226, 227	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
229	228	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
230	199	ffvelrni 6960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 ∈ dom 𝑂 → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
231	145, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝐺 supp ∅))
232	198, 231	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ 𝐵)
233		onelon 6291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝐵 ∈ On ∧ (𝑂‘𝑢) ∈ 𝐵) → (𝑂‘𝑢) ∈ On)
234	10, 232, 233	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ On)
235	234	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑂‘𝑢) ∈ On)
236		onsssuc 6353	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
237	225, 235, 236	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ suc (𝑂‘𝑢)))
238		vex 3436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑢 ∈ V
239	238	sucid 6345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ 𝑢 ∈ suc 𝑢
240	46	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
241		isorel 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
242	240, 145, 143, 241	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 E suc 𝑢 ↔ (𝑂‘𝑢) E (𝑂‘suc 𝑢)))
243	238	sucex 7656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ suc 𝑢 ∈ V
244	243	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑢 E suc 𝑢 ↔ 𝑢 ∈ suc 𝑢)
245		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑂‘suc 𝑢) ∈ V
246	245	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘𝑢) E (𝑂‘suc 𝑢) ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
247	242, 244, 246	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑢 ∈ suc 𝑢 ↔ (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢)))
248	239, 247	mpbii 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘𝑢) ∈ (𝑂‘suc 𝑢))
249		eloni 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘suc 𝑢) ∈ On → Ord (𝑂‘suc 𝑢))
250	204, 249	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → Ord (𝑂‘suc 𝑢))
251		ordelsuc 7667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝑂‘𝑢) ∈ On ∧ Ord (𝑂‘suc 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
252	234, 250, 251	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑂‘𝑢) ∈ (𝑂‘suc 𝑢) ↔ suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢)))
253	248, 252	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
254	253	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → suc (𝑂‘𝑢) ⊆ (𝑂‘suc 𝑢))
255	254	sseld 3920	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ suc (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
256	237, 255	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) → 𝑥 ∈ (𝑂‘suc 𝑢)))
257		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ 𝑥)
258	240	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑥 ∈ (𝐺 supp ∅))
261		f1ocnvfv2 7149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
262	259, 260, 261	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
263	257, 262	eleqtrrd 2842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥)))
264	145	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ dom 𝑂)
265	259, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
266	265, 260	ffvelrnd 6962	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
267		isorel 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂)) → (𝑢 E (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥))))
268	258, 264, 266, 267	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 E (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥))))
269		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (^◡𝑂‘𝑥) ∈ V
270	269	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑢 E (^◡𝑂‘𝑥) ↔ 𝑢 ∈ (^◡𝑂‘𝑥))
271		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑂‘(^◡𝑂‘𝑥)) ∈ V
272	271	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑂‘𝑢) E (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥)))
273	268, 270, 272	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘𝑢) ∈ (𝑂‘(^◡𝑂‘𝑥))))
274	263, 273	mpbird 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → 𝑢 ∈ (^◡𝑂‘𝑥))
275		ordelon 6290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((Ord dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂) → (^◡𝑂‘𝑥) ∈ On)
276	36, 266, 275	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (^◡𝑂‘𝑥) ∈ On)
277		eloni 6276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((^◡𝑂‘𝑥) ∈ On → Ord (^◡𝑂‘𝑥))
278	276, 277	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → Ord (^◡𝑂‘𝑥))
279		ordelsuc 7667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑢 ∈ (^◡𝑂‘𝑥) ∧ Ord (^◡𝑂‘𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (^◡𝑂‘𝑥)))
280	274, 278, 279	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (𝑢 ∈ (^◡𝑂‘𝑥) ↔ suc 𝑢 ⊆ (^◡𝑂‘𝑥)))
281	274, 280	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ⊆ (^◡𝑂‘𝑥))
282	143	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ dom 𝑂)
283	36, 282, 131	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → suc 𝑢 ∈ On)
284		ontri1 6300	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((suc 𝑢 ∈ On ∧ (^◡𝑂‘𝑥) ∈ On) → (suc 𝑢 ⊆ (^◡𝑂‘𝑥) ↔ ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢))
285	283, 276, 284	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → (suc 𝑢 ⊆ (^◡𝑂‘𝑥) ↔ ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢))
286	281, 285	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ (^◡𝑂‘𝑥) ∈ suc 𝑢)
287		isorel 7197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((^◡𝑂‘𝑥) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
288	258, 266, 282, 287	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢)))
289	243	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((^◡𝑂‘𝑥) E suc 𝑢 ↔ (^◡𝑂‘𝑥) ∈ suc 𝑢)
290	245	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑂‘(^◡𝑂‘𝑥)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢))
291	288, 289, 290	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) ∈ suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢)))
292	262	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((𝑂‘(^◡𝑂‘𝑥)) ∈ (𝑂‘suc 𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
293	291, 292	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ((^◡𝑂‘𝑥) ∈ suc 𝑢 ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
294	286, 293	mtbid 324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ ((𝐹‘𝑥) ≠ ∅ ∧ (𝑂‘𝑢) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝑂‘suc 𝑢))
295	294	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑂‘𝑢) ∈ 𝑥 → ¬ 𝑥 ∈ (𝑂‘suc 𝑢)))
296	295	con2d 134	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → ¬ (𝑂‘𝑢) ∈ 𝑥))
297		ontri1 6300	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑥 ∈ On ∧ (𝑂‘𝑢) ∈ On) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
298	225, 235, 297	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ ¬ (𝑂‘𝑢) ∈ 𝑥))
299	296, 298	sylibrd 258	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ∈ (𝑂‘suc 𝑢) → 𝑥 ⊆ (𝑂‘𝑢)))
300	256, 299	impbid 211	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑥 ∈ (𝑂‘suc 𝑢)))
301	300	orbi1d 914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 ∈ (𝑂‘suc 𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
302	229, 301	bitr4d 281	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢))))
303		orcom 867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑥 ⊆ (𝑂‘𝑢) ∨ 𝑥 = (𝑂‘suc 𝑢)) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)))
304	302, 303	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → (𝑥 ⊆ (𝑂‘suc 𝑢) ↔ (𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢))))
305	304	ifbid 4482	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) ∧ (𝐹‘𝑥) ≠ ∅) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
306		eqidd 2739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ∅ = ∅)
307	221, 305, 306	pm2.61ne 3030	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅) = if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))
308	307	mpteq2dva 5174	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)))
309	308	fveq2d 6778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))))
310		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑥) ∈ V
311	310, 175	ifex 4509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V
312	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
313	312	ralrimivw 3104	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑥 ∈ 𝐵 if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
314		eqid 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
315	314	fnmpt 6573	. . . . . . . . . . . . . . . . . . . . . . . 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 7985	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅})
319		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦𝐵
320		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥𝐵
321		nffvmpt1 6785	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)
322		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑥∅
323	321, 322	nfne 3045	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑥((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅
324		nfv 1917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑦((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅
325		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑦 = 𝑥 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥))
326	325	neeq1d 3003	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑥 → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅ ↔ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅))
327	319, 320, 323, 324, 326	cbvrabw 3424	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑦 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅}
328	318, 327	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) Fn 𝐵 ∧ 𝐵 ∈ On ∧ ∅ ∈ V) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
329	316, 148, 317, 328	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅})
330		eqidd 2739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))
331	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V)
332	330, 331	fvmpt2d 6888	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) = if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))
333	332	neeq1d 3003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
334	331	biantrurd 533	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)))
335		dif1o 8330	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) ↔ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ V ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅))
336	334, 335	bitr4di 289	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)))
337	333, 336	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅ ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)))
338	337	rabbidva 3413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑥) ≠ ∅} = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)})
339	329, 338	eqtrd 2778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) = {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)})
340	311, 335	mpbiran 706	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) ↔ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅)
341		ifeq1 4463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘𝑢), ∅, ∅))
342	341, 179	eqtrdi 2794	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐹‘𝑥) = ∅ → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
343	342	necon3i 2976	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → (𝐹‘𝑥) ≠ ∅)
344		iffalse 4468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (¬ 𝑥 ⊆ (𝑂‘𝑢) → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = ∅)
345	344	necon1ai 2971	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ⊆ (𝑂‘𝑢))
346	343, 345	jca 512	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → ((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)))
347	256	expimpd 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (((𝐹‘𝑥) ≠ ∅ ∧ 𝑥 ⊆ (𝑂‘𝑢)) → 𝑥 ∈ (𝑂‘suc 𝑢)))
348	346, 347	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ≠ ∅ → 𝑥 ∈ (𝑂‘suc 𝑢)))
349	340, 348	syl5bi 241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵) → (if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o) → 𝑥 ∈ (𝑂‘suc 𝑢)))
350	349	3impia 1116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) ∧ 𝑥 ∈ 𝐵 ∧ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)) → 𝑥 ∈ (𝑂‘suc 𝑢))
351	350	rabssdv 4008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → {𝑥 ∈ 𝐵 ∣ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) ∈ (V ∖ 1_o)} ⊆ (𝑂‘suc 𝑢))
352	339, 351	eqsstrd 3959	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)) supp ∅) ⊆ (𝑂‘suc 𝑢))
353		eqeq1 2742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 = (𝑂‘suc 𝑢) ↔ 𝑦 = (𝑂‘suc 𝑢)))
354		sseq1 3946	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑦 → (𝑥 ⊆ (𝑂‘𝑢) ↔ 𝑦 ⊆ (𝑂‘𝑢)))
355	353, 354	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → ((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)) ↔ (𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢))))
356		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
357	355, 356	ifbieq1d 4483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑦 → if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
358	357	cbvmptv 5187	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
359		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = (𝑂‘suc 𝑢) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
360	359	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑦 = (𝑂‘suc 𝑢)) → (𝐹‘𝑦) = (𝐹‘(𝑂‘suc 𝑢)))
361	360	ifeq1da 4490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
362	354, 356	ifbieq1d 4483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = 𝑦 → if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
363		fvex 6787	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐹‘𝑦) ∈ V
364	363, 175	ifex 4509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅) ∈ V
365	362, 314, 364	fvmpt 6875	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 ∈ 𝐵 → ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦) = if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
366	365	ifeq2d 4479	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅)))
367		ifor 4513	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅) = if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), if(𝑦 ⊆ (𝑂‘𝑢), (𝐹‘𝑦), ∅))
368	366, 367	eqtr4di 2796	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘𝑦), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
369	361, 368	eqtr3d 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ 𝐵 → if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)) = if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
370	369	mpteq2ia 5177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if((𝑦 = (𝑂‘suc 𝑢) ∨ 𝑦 ⊆ (𝑂‘𝑢)), (𝐹‘𝑦), ∅))
371	358, 370	eqtr4i 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = (𝑂‘suc 𝑢), (𝐹‘(𝑂‘suc 𝑢)), ((𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))‘𝑦)))
372	8, 151, 148, 186, 202, 208, 352, 371	cantnfp1 9439	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅)) ∈ 𝑆 ∧ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))))))
373	372	simprd 496	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if((𝑥 = (𝑂‘suc 𝑢) ∨ 𝑥 ⊆ (𝑂‘𝑢)), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
374	309, 373	eqtrd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅)))))
375	8, 9, 10, 2, 13, 113	cantnfsuc 9428	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ suc 𝑢 ∈ ω) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
376	192, 375	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
377	160	simp3d 1143	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
378	377	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
379	108	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(^◡𝑂‘𝑋)) = 𝑋)
380	136	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑢 ∈ On)
381		onsssuc 6353	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((^◡𝑂‘𝑋) ∈ On ∧ 𝑢 ∈ On) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
382	129, 380, 381	syl2an2r 682	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) ⊆ 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢))
383	146, 382	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ∈ suc 𝑢)
384	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (^◡𝑂‘𝑋) ∈ dom 𝑂)
385		isorel 7197	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ ((^◡𝑂‘𝑋) ∈ dom 𝑂 ∧ suc 𝑢 ∈ dom 𝑂)) → ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
386	240, 384, 143, 385	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢)))
387	243	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((^◡𝑂‘𝑋) E suc 𝑢 ↔ (^◡𝑂‘𝑋) ∈ suc 𝑢)
388	245	epeli 5497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂‘(^◡𝑂‘𝑋)) E (𝑂‘suc 𝑢) ↔ (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
389	386, 387, 388	3bitr3g 313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((^◡𝑂‘𝑋) ∈ suc 𝑢 ↔ (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢)))
390	383, 389	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝑂‘(^◡𝑂‘𝑋)) ∈ (𝑂‘suc 𝑢))
391	379, 390	eqeltrrd 2840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → 𝑋 ∈ (𝑂‘suc 𝑢))
392		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ (𝑂‘suc 𝑢)))
393		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐹‘𝑤) = (𝐹‘(𝑂‘suc 𝑢)))
394		fveq2 6774	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑂‘suc 𝑢) → (𝐺‘𝑤) = (𝐺‘(𝑂‘suc 𝑢)))
395	393, 394	eqeq12d 2754	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢))))
396	392, 395	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = (𝑂‘suc 𝑢) → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
397	396	rspcv 3557	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑂‘suc 𝑢) ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ (𝑂‘suc 𝑢) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))))
398	202, 378, 391, 397	syl3c 66	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐹‘(𝑂‘suc 𝑢)) = (𝐺‘(𝑂‘suc 𝑢)))
399	398	oveq2d 7291	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) = ((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))))
400	399	oveq1d 7290	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐺‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
401	376, 400	eqtr4d 2781	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (𝐻‘suc suc 𝑢) = (((𝐴 ↑_o (𝑂‘suc 𝑢)) ·_o (𝐹‘(𝑂‘suc 𝑢))) +_o (𝐻‘suc 𝑢)))
402	374, 401	eleq12d 2833	. . . . . . . . . . . . . . . 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 281	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
404	403	biimpd 228	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
405	147, 404	embantd 59	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (suc 𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢)) → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
406	405	expr 457	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
407	140, 406	sylbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ∈ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
408		fveq2 6774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑂‘(^◡𝑂‘𝑋)) = (𝑂‘suc 𝑢))
409	408	sseq2d 3953	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)) ↔ 𝑥 ⊆ (𝑂‘suc 𝑢)))
410	409	ifbid 4482	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅) = if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))
411	410	mpteq2dv 5176	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅)))
412	411	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))))
413		suceq 6331	. . . . . . . . . . . . . . . 16 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → suc (^◡𝑂‘𝑋) = suc suc 𝑢)
414	413	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (𝐻‘suc (^◡𝑂‘𝑋)) = (𝐻‘suc suc 𝑢))
415	412, 414	eleq12d 2833	. . . . . . . . . . . . . 14 ⊢ ((^◡𝑂‘𝑋) = suc 𝑢 → (((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘(^◡𝑂‘𝑋)), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc (^◡𝑂‘𝑋)) ↔ ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
416	115, 415	syl5ibcom 244	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((^◡𝑂‘𝑋) = suc 𝑢 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢)))
417	416	adantr 481	. . . . . . . . . . . 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 239	. . . . . . . . 9 ⊢ ((𝜑 ∧ suc 𝑢 ∈ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ suc 𝑢 → (((𝑢 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑢) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑢)) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘suc 𝑢), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc suc 𝑢))))
421	420	expimpd 454	. . . . . . . 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 7747	. . . . 5 ⊢ (𝑦 ∈ ω → (𝜑 → ((𝑦 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ⊆ 𝑦) → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘𝑦), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc 𝑦))))
425	70, 424	vtoclga 3513	. . . 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 696	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))) ∈ (𝐻‘suc ∪ dom 𝑂))
428	155	feqmptd 6837	. . . 4 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)))
429		eqeq2 2750	. . . . . 6 ⊢ ((𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
430		eqeq2 2750	. . . . . 6 ⊢ (∅ = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅) → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
431		eqidd 2739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = (𝐹‘𝑥))
432	199	ffvelrni 6960	. . . . . . . . . . . . . 14 ⊢ (∪ dom 𝑂 ∈ dom 𝑂 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
433	44, 432	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ (𝐺 supp ∅))
434	197, 433	sseldd 3922	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ 𝐵)
435		onelon 6291	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
436	10, 434, 435	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑂‘∪ dom 𝑂) ∈ On)
437	436	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂‘∪ dom 𝑂) ∈ On)
438		ontri1 6300	. . . . . . . . . 10 ⊢ ((𝑥 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
439	224, 437, 438	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
440	439	con2bid 355	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 ↔ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)))
441		simprl 768	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ 𝐵)
442	377	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))
443		eloni 6276	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂‘𝑋) ∈ On → Ord (^◡𝑂‘𝑋))
444	129, 443	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → Ord (^◡𝑂‘𝑋))
445		orduni 7639	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord dom 𝑂 → Ord ∪ dom 𝑂)
446	36, 445	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ Ord ∪ dom 𝑂
447		ordtri1 6299	. . . . . . . . . . . . . . . . 17 ⊢ ((Ord (^◡𝑂‘𝑋) ∧ Ord ∪ dom 𝑂) → ((^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋)))
448	444, 446, 447	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((^◡𝑂‘𝑋) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋)))
449	54, 448	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋))
450		isorel 7197	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑋) ∈ dom 𝑂)) → (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋))))
451	46, 44, 52, 450	syl12anc 834	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋))))
452		fvex 6787	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝑂‘𝑋) ∈ V
453	452	epeli 5497	. . . . . . . . . . . . . . . . 17 ⊢ (∪ dom 𝑂 E (^◡𝑂‘𝑋) ↔ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑋))
454		fvex 6787	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑂‘(^◡𝑂‘𝑋)) ∈ V
455	454	epeli 5497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋)))
456	451, 453, 455	3bitr3g 313	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋))))
457	108	eleq2d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑋)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
458	456, 457	bitrd 278	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑋) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
459	449, 458	mtbid 324	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋)
460		onelon 6291	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ∈ On ∧ 𝑋 ∈ 𝐵) → 𝑋 ∈ On)
461	10, 161, 460	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑋 ∈ On)
462		ontri1 6300	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ On ∧ (𝑂‘∪ dom 𝑂) ∈ On) → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
463	461, 436, 462	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋 ⊆ (𝑂‘∪ dom 𝑂) ↔ ¬ (𝑂‘∪ dom 𝑂) ∈ 𝑋))
464	459, 463	mpbird 256	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
465	464	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ⊆ (𝑂‘∪ dom 𝑂))
466		simprr 770	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
467	224	adantrr 714	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ On)
468		ontr2 6313	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ On ∧ 𝑥 ∈ On) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
469	461, 467, 468	syl2an2r 682	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ((𝑋 ⊆ (𝑂‘∪ dom 𝑂) ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥) → 𝑋 ∈ 𝑥))
470	465, 466, 469	mp2and 696	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑋 ∈ 𝑥)
471		eleq2 2827	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → (𝑋 ∈ 𝑤 ↔ 𝑋 ∈ 𝑥))
472		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
473		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → (𝐺‘𝑤) = (𝐺‘𝑥))
474	472, 473	eqeq12d 2754	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑥 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑥) = (𝐺‘𝑥)))
475	471, 474	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑥 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
476	475	rspcv 3557	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐵 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) → (𝑋 ∈ 𝑥 → (𝐹‘𝑥) = (𝐺‘𝑥))))
477	441, 442, 470, 476	syl3c 66	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = (𝐺‘𝑥))
478	466	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘∪ dom 𝑂) ∈ 𝑥)
479	46	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)))
480	44	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ dom 𝑂)
481	51	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂)
482		ffvelrn 6959	. . . . . . . . . . . . . . . . . 18 ⊢ ((^◡𝑂:(𝐺 supp ∅)⟶dom 𝑂 ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
483	481, 482	sylancom 588	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ dom 𝑂)
484		isorel 7197	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑂 Isom E , E (dom 𝑂, (𝐺 supp ∅)) ∧ (∪ dom 𝑂 ∈ dom 𝑂 ∧ (^◡𝑂‘𝑥) ∈ dom 𝑂)) → (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥))))
485	479, 480, 483, 484	syl12anc 834	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥))))
486	269	epeli 5497	. . . . . . . . . . . . . . . 16 ⊢ (∪ dom 𝑂 E (^◡𝑂‘𝑥) ↔ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
487	271	epeli 5497	. . . . . . . . . . . . . . . 16 ⊢ ((𝑂‘∪ dom 𝑂) E (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥)))
488	485, 486, 487	3bitr3g 313	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥))))
489	48	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → 𝑂:dom 𝑂–1-1-onto→(𝐺 supp ∅))
490	489, 261	sylancom 588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (𝑂‘(^◡𝑂‘𝑥)) = 𝑥)
491	490	eleq2d 2824	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((𝑂‘∪ dom 𝑂) ∈ (𝑂‘(^◡𝑂‘𝑥)) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
492	488, 491	bitrd 278	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (∪ dom 𝑂 ∈ (^◡𝑂‘𝑥) ↔ (𝑂‘∪ dom 𝑂) ∈ 𝑥))
493	478, 492	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
494		elssuni 4871	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝑂‘𝑥) ∈ dom 𝑂 → (^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
495	483, 494	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂)
496	36, 483, 275	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → (^◡𝑂‘𝑥) ∈ On)
497	496, 277	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → Ord (^◡𝑂‘𝑥))
498		ordtri1 6299	. . . . . . . . . . . . . . 15 ⊢ ((Ord (^◡𝑂‘𝑥) ∧ Ord ∪ dom 𝑂) → ((^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥)))
499	497, 446, 498	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ((^◡𝑂‘𝑥) ⊆ ∪ dom 𝑂 ↔ ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥)))
500	495, 499	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) ∧ 𝑥 ∈ (𝐺 supp ∅)) → ¬ ∪ dom 𝑂 ∈ (^◡𝑂‘𝑥))
501	493, 500	pm2.65da 814	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → ¬ 𝑥 ∈ (𝐺 supp ∅))
502	441, 501	eldifd 3898	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅)))
503		ssidd 3944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐺 supp ∅) ⊆ (𝐺 supp ∅))
504	159, 503, 10, 176	suppssr 8012	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ (𝐺 supp ∅))) → (𝐺‘𝑥) = ∅)
505	502, 504	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐺‘𝑥) = ∅)
506	477, 505	eqtrd 2778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ (𝑂‘∪ dom 𝑂) ∈ 𝑥)) → (𝐹‘𝑥) = ∅)
507	506	expr 457	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑂‘∪ dom 𝑂) ∈ 𝑥 → (𝐹‘𝑥) = ∅))
508	440, 507	sylbird 259	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂) → (𝐹‘𝑥) = ∅))
509	508	imp 407	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ ¬ 𝑥 ⊆ (𝑂‘∪ dom 𝑂)) → (𝐹‘𝑥) = ∅)
510	429, 430, 431, 509	ifbothda 4497	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐹‘𝑥) = if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))
511	510	mpteq2dva 5174	. . . 4 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
512	428, 511	eqtrd 2778	. . 3 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅)))
513	512	fveq2d 6778	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = ((𝐴 CNF 𝐵)‘(𝑥 ∈ 𝐵 ↦ if(𝑥 ⊆ (𝑂‘∪ dom 𝑂), (𝐹‘𝑥), ∅))))
514	8, 9, 10, 2, 13, 113	cantnfval 9426	. . 3 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘dom 𝑂))
515	43	fveq2d 6778	. . 3 ⊢ (𝜑 → (𝐻‘dom 𝑂) = (𝐻‘suc ∪ dom 𝑂))
516	514, 515	eqtrd 2778	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐺) = (𝐻‘suc ∪ dom 𝑂))
517	427, 513, 516	3eltr4d 2854	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘𝐺))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∀wral 3064 ∃wrex 3065 {crab 3068 Vcvv 3432 ∖ cdif 3884 ⊆ wss 3887 ∅c0 4256 ifcif 4459 ∪ cuni 4839 class class class wbr 5074 {copab 5136 ↦ cmpt 5157 Tr wtr 5191 E cep 5494 We wwe 5543 ^◡ccnv 5588 dom cdm 5589 Ord word 6265 Oncon0 6266 Lim wlim 6267 suc csuc 6268 Fun wfun 6427 Fn wfn 6428 ⟶wf 6429 –1-1-onto→wf1o 6432 ‘cfv 6433 Isom wiso 6434 (class class class)co 7275 ∈ cmpo 7277 ωcom 7712 supp csupp 7977 seq_ωcseqom 8278 1_oc1o 8290 +_o coa 8294 ·_o comu 8295 ↑_o coe 8296 ≈ cen 8730 finSupp cfsupp 9128 OrdIsocoi 9268 CNF ccnf 9419

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5209 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rmo 3071 df-reu 3072 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-tr 5192 df-id 5489 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-se 5545 df-we 5546 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-f1 6438 df-fo 6439 df-f1o 6440 df-fv 6441 df-isom 6442 df-riota 7232 df-ov 7278 df-oprab 7279 df-mpo 7280 df-om 7713 df-1st 7831 df-2nd 7832 df-supp 7978 df-frecs 8097 df-wrecs 8128 df-recs 8202 df-rdg 8241 df-seqom 8279 df-1o 8297 df-2o 8298 df-oadd 8301 df-omul 8302 df-oexp 8303 df-er 8498 df-map 8617 df-en 8734 df-dom 8735 df-sdom 8736 df-fin 8737 df-fsupp 9129 df-oi 9269 df-cnf 9420

This theorem is referenced by: cantnf 9451

W3C validator