Theorem cnfcom2lem 9622

Description: Lemma for cnfcom2 9623. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)

Hypotheses

Ref	Expression
cnfcom.s	⊢ 𝑆 = dom (ω CNF 𝐴)
cnfcom.a	⊢ (𝜑 → 𝐴 ∈ On)
cnfcom.b	⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
cnfcom.f	⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
cnfcom.g	⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
cnfcom.h	⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (𝑀 +o 𝑧)), ∅)
cnfcom.t	⊢ 𝑇 = seqω((𝑘 ∈ V, 𝑓 ∈ V ↦ 𝐾), ∅)
cnfcom.m	⊢ 𝑀 = ((ω ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘)))
cnfcom.k	⊢ 𝐾 = ((𝑥 ∈ 𝑀 ↦ (dom 𝑓 +o 𝑥)) ∪ ◡(𝑥 ∈ dom 𝑓 ↦ (𝑀 +o 𝑥)))
cnfcom.w	⊢ 𝑊 = (𝐺‘∪ dom 𝐺)
cnfcom2.1	⊢ (𝜑 → ∅ ∈ 𝐵)

Assertion

Ref	Expression
cnfcom2lem	⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)

Distinct variable groups:   𝑥,𝑘,𝑧,𝐴   𝑥,𝑀   𝑓,𝑘,𝑥,𝑧,𝐹   𝑧,𝑇   𝑥,𝑊   𝑓,𝐺,𝑘,𝑥,𝑧   𝑓,𝐻,𝑥   𝑆,𝑘,𝑧   𝜑,𝑘,𝑥,𝑧

Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑓)   𝐵(𝑥,𝑧,𝑓,𝑘)   𝑆(𝑥,𝑓)   𝑇(𝑥,𝑓,𝑘)   𝐻(𝑧,𝑘)   𝐾(𝑥,𝑧,𝑓,𝑘)   𝑀(𝑧,𝑓,𝑘)   𝑊(𝑧,𝑓,𝑘)

Proof of Theorem cnfcom2lem

Step	Hyp	Ref	Expression
1		cnfcom2.1	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝐵)
2		n0i 4280	. . . . . 6 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → ¬ 𝐵 = ∅)
4		cnfcom.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9567	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ω ∈ On)
8		cnfcom.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ On)
9	5, 7, 8	cantnff1o 9617	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴))
10		f1ocnv 6792	. . . . . . . . . . . . . . . 16 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) → ◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆)
11		f1of 6780	. . . . . . . . . . . . . . . 16 ⊢ (◡(ω CNF 𝐴):(ω ↑o 𝐴)–1-1-onto→𝑆 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
12	9, 10, 11	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ◡(ω CNF 𝐴):(ω ↑o 𝐴)⟶𝑆)
13		cnfcom.b	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐵 ∈ (ω ↑o 𝐴))
14	12, 13	ffvelcdmd 7037	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
15	4, 14	eqeltrid 2840	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
16	5, 7, 8	cantnfs 9587	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
17	15, 16	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
18	17	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
19	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹:𝐴⟶ω)
20	19	feqmptd 6908	. . . . . . . . 9 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
21		dif0 4318	. . . . . . . . . . . 12 ⊢ (𝐴 ∖ ∅) = 𝐴
22	21	eleq2i 2828	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ∅) ↔ 𝑥 ∈ 𝐴)
23		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 = ∅)
24		ovexd 7402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
25		cnfcom.g	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
26	5, 7, 8, 25, 15	cantnfcl 9588	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
27	26	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → E We (𝐹 supp ∅))
28	25	oien 9453	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → dom 𝐺 ≈ (𝐹 supp ∅))
29	24, 27, 28	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐺 ≈ (𝐹 supp ∅))
30	29	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 ≈ (𝐹 supp ∅))
31	23, 30	eqbrtrrd 5109	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ≈ (𝐹 supp ∅))
32	31	ensymd 8952	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ≈ ∅)
33		en0 8965	. . . . . . . . . . . . . 14 ⊢ ((𝐹 supp ∅) ≈ ∅ ↔ (𝐹 supp ∅) = ∅)
34	32, 33	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) = ∅)
35		ss0b 4341	. . . . . . . . . . . . 13 ⊢ ((𝐹 supp ∅) ⊆ ∅ ↔ (𝐹 supp ∅) = ∅)
36	34, 35	sylibr 234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ⊆ ∅)
37	8	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐴 ∈ On)
38		0ex 5242	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
39	38	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ∈ V)
40	19, 36, 37, 39	suppssr 8145	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ (𝐴 ∖ ∅)) → (𝐹‘𝑥) = ∅)
41	22, 40	sylan2br 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ∅)
42	41	mpteq2dva 5178	. . . . . . . . 9 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ ∅))
43	20, 42	eqtrd 2771	. . . . . . . 8 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ ∅))
44		fconstmpt 5693	. . . . . . . 8 ⊢ (𝐴 × {∅}) = (𝑥 ∈ 𝐴 ↦ ∅)
45	43, 44	eqtr4di 2789	. . . . . . 7 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝐴 × {∅}))
46	45	fveq2d 6844	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(𝐴 × {∅})))
47	4	fveq2i 6843	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵))
48		f1ocnvfv2 7232	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑o 𝐴) ∧ 𝐵 ∈ (ω ↑o 𝐴)) → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
49	9, 13, 48	syl2anc 585	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
50	47, 49	eqtrid 2783	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵)
51	50	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵)
52		peano1 7840	. . . . . . . . 9 ⊢ ∅ ∈ ω
53	52	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ ω)
54	5, 7, 8, 53	cantnf0 9596	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘(𝐴 × {∅})) = ∅)
55	54	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘(𝐴 × {∅})) = ∅)
56	46, 51, 55	3eqtr3d 2779	. . . . 5 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐵 = ∅)
57	3, 56	mtand 816	. . . 4 ⊢ (𝜑 → ¬ dom 𝐺 = ∅)
58		nnlim 7831	. . . . 5 ⊢ (dom 𝐺 ∈ ω → ¬ Lim dom 𝐺)
59	26, 58	simpl2im 503	. . . 4 ⊢ (𝜑 → ¬ Lim dom 𝐺)
60		ioran 986	. . . 4 ⊢ (¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺) ↔ (¬ dom 𝐺 = ∅ ∧ ¬ Lim dom 𝐺))
61	57, 59, 60	sylanbrc 584	. . 3 ⊢ (𝜑 → ¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))
62	25	oicl 9444	. . . 4 ⊢ Ord dom 𝐺
63		unizlim 6447	. . . 4 ⊢ (Ord dom 𝐺 → (dom 𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)))
64	62, 63	ax-mp 5	. . 3 ⊢ (dom 𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))
65	61, 64	sylnibr 329	. 2 ⊢ (𝜑 → ¬ dom 𝐺 = ∪ dom 𝐺)
66		orduniorsuc 7781	. . . 4 ⊢ (Ord dom 𝐺 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺))
67	62, 66	mp1i 13	. . 3 ⊢ (𝜑 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺))
68	67	ord 865	. 2 ⊢ (𝜑 → (¬ dom 𝐺 = ∪ dom 𝐺 → dom 𝐺 = suc ∪ dom 𝐺))
69	65, 68	mpd 15	1 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889  ∅c0 4273  {csn 4567  ∪ cuni 4850   class class class wbr 5085   ↦ cmpt 5166   E cep 5530   We wwe 5583   × cxp 5629  ^◡ccnv 5630  dom cdm 5631  Ord word 6322  Oncon0 6323  Lim wlim 6324  suc csuc 6325  ⟶wf 6494  –1-1-onto→wf1o 6497  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  ωcom 7817   supp csupp 8110  seq_ωcseqom 8386   +_o coa 8402   ·_o comu 8403   ↑_o coe 8404   ≈ cen 8890   finSupp cfsupp 9274  OrdIsocoi 9424   CNF ccnf 9582

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-inf2 9562

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-seqom 8387  df-1o 8405  df-2o 8406  df-oadd 8409  df-omul 8410  df-oexp 8411  df-er 8643  df-map 8775  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-oi 9425  df-cnf 9583

This theorem is referenced by:  cnfcom2  9623  cnfcom3lem  9624  cnfcom3  9625