cnfcom2lem - Metamath Proof Explorer

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

Theorem cnfcom2lem 9650

Description: Lemma for cnfcom2 9651. (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 4290	. . . . . 6 ⊢ (∅ ∈ 𝐵 → ¬ 𝐵 = ∅)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → ¬ 𝐵 = ∅)
4		cnfcom.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (^◡(ω CNF 𝐴)‘𝐵)
5		cnfcom.s	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 = dom (ω CNF 𝐴)
6		omelon 9595	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ On
7	6	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ω ∈ On)
8		cnfcom.a	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐴 ∈ On)
9	5, 7, 8	cantnff1o 9645	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴))
10		f1ocnv 6814	. . . . . . . . . . . . . . . 16 ⊢ ((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴) → ^◡(ω CNF 𝐴):(ω ↑_o 𝐴)–1-1-onto→𝑆)
11		f1of 6801	. . . . . . . . . . . . . . . 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 7061	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (^◡(ω CNF 𝐴)‘𝐵) ∈ 𝑆)
15	4, 14	eqeltrid 2865	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ 𝑆)
16	5, 7, 8	cantnfs 9615	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅)))
17	15, 16	mpbid 234	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹:𝐴⟶ω ∧ 𝐹 finSupp ∅))
18	17	simpld 498	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:𝐴⟶ω)
19	18	adantr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹:𝐴⟶ω)
20	19	feqmptd 6930	. . . . . . . . 9 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
21		dif0 4328	. . . . . . . . . . . 12 ⊢ (𝐴 ∖ ∅) = 𝐴
22	21	eleq2i 2853	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 ∖ ∅) ↔ 𝑥 ∈ 𝐴)
23		simpr 488	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 = ∅)
24		ovexd 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 supp ∅) ∈ V)
25		cnfcom.g	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅))
26	5, 7, 8, 25, 15	cantnfcl 9616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω))
27	26	simpld 498	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → E We (𝐹 supp ∅))
28	25	oien 9480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 supp ∅) ∈ V ∧ E We (𝐹 supp ∅)) → dom 𝐺 ≈ (𝐹 supp ∅))
29	24, 27, 28	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → dom 𝐺 ≈ (𝐹 supp ∅))
30	29	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → dom 𝐺 ≈ (𝐹 supp ∅))
31	23, 30	eqbrtrrd 5121	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ≈ (𝐹 supp ∅))
32	31	ensymd 8980	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ≈ ∅)
33		en0 8993	. . . . . . . . . . . . . 14 ⊢ ((𝐹 supp ∅) ≈ ∅ ↔ (𝐹 supp ∅) = ∅)
34	32, 33	sylib 220	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) = ∅)
35		ss0b 4352	. . . . . . . . . . . . 13 ⊢ ((𝐹 supp ∅) ⊆ ∅ ↔ (𝐹 supp ∅) = ∅)
36	34, 35	sylibr 236	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝐹 supp ∅) ⊆ ∅)
37	8	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐴 ∈ On)
38		0ex 5254	. . . . . . . . . . . . 13 ⊢ ∅ ∈ V
39	38	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ∅ ∈ V)
40	19, 36, 37, 39	suppssr 8169	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ (𝐴 ∖ ∅)) → (𝐹‘𝑥) = ∅)
41	22, 40	sylan2br 604	. . . . . . . . . 10 ⊢ (((𝜑 ∧ dom 𝐺 = ∅) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = ∅)
42	41	mpteq2dva 5190	. . . . . . . . 9 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ ∅))
43	20, 42	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝑥 ∈ 𝐴 ↦ ∅))
44		fconstmpt 5705	. . . . . . . 8 ⊢ (𝐴 × {∅}) = (𝑥 ∈ 𝐴 ↦ ∅)
45	43, 44	eqtr4di 2814	. . . . . . 7 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐹 = (𝐴 × {∅}))
46	45	fveq2d 6866	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(𝐴 × {∅})))
47	4	fveq2i 6865	. . . . . . . 8 ⊢ ((ω CNF 𝐴)‘𝐹) = ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵))
48		f1ocnvfv2 7256	. . . . . . . . 9 ⊢ (((ω CNF 𝐴):𝑆–1-1-onto→(ω ↑_o 𝐴) ∧ 𝐵 ∈ (ω ↑_o 𝐴)) → ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
49	9, 13, 48	syl2anc 593	. . . . . . . 8 ⊢ (𝜑 → ((ω CNF 𝐴)‘(^◡(ω CNF 𝐴)‘𝐵)) = 𝐵)
50	47, 49	eqtrid 2808	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘𝐹) = 𝐵)
51	50	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘𝐹) = 𝐵)
52		peano1 7864	. . . . . . . . 9 ⊢ ∅ ∈ ω
53	52	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ∅ ∈ ω)
54	5, 7, 8, 53	cantnf0 9624	. . . . . . 7 ⊢ (𝜑 → ((ω CNF 𝐴)‘(𝐴 × {∅})) = ∅)
55	54	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → ((ω CNF 𝐴)‘(𝐴 × {∅})) = ∅)
56	46, 51, 55	3eqtr3d 2804	. . . . 5 ⊢ ((𝜑 ∧ dom 𝐺 = ∅) → 𝐵 = ∅)
57	3, 56	mtand 825	. . . 4 ⊢ (𝜑 → ¬ dom 𝐺 = ∅)
58		nnlim 7855	. . . . 5 ⊢ (dom 𝐺 ∈ ω → ¬ Lim dom 𝐺)
59	26, 58	simpl2im 511	. . . 4 ⊢ (𝜑 → ¬ Lim dom 𝐺)
60		ioran 996	. . . 4 ⊢ (¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺) ↔ (¬ dom 𝐺 = ∅ ∧ ¬ Lim dom 𝐺))
61	57, 59, 60	sylanbrc 592	. . 3 ⊢ (𝜑 → ¬ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))
62	25	oicl 9471	. . . 4 ⊢ Ord dom 𝐺
63		unizlim 6465	. . . 4 ⊢ (Ord dom 𝐺 → (dom 𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺)))
64	62, 63	ax-mp 5	. . 3 ⊢ (dom 𝐺 = ∪ dom 𝐺 ↔ (dom 𝐺 = ∅ ∨ Lim dom 𝐺))
65	61, 64	sylnibr 331	. 2 ⊢ (𝜑 → ¬ dom 𝐺 = ∪ dom 𝐺)
66		orduniorsuc 7805	. . . 4 ⊢ (Ord dom 𝐺 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺))
67	62, 66	mp1i 13	. . 3 ⊢ (𝜑 → (dom 𝐺 = ∪ dom 𝐺 ∨ dom 𝐺 = suc ∪ dom 𝐺))
68	67	ord 875	. 2 ⊢ (𝜑 → (¬ dom 𝐺 = ∪ dom 𝐺 → dom 𝐺 = suc ∪ dom 𝐺))
69	65, 68	mpd 15	1 ⊢ (𝜑 → dom 𝐺 = suc ∪ dom 𝐺)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 ∅c0 4283 {csn 4579 ∪ cuni 4862 class class class wbr 5097 ↦ cmpt 5178 E cep 5542 We wwe 5595 × cxp 5641 ^◡ccnv 5642 dom cdm 5643 Ord word 6340 Oncon0 6341 Lim wlim 6342 suc csuc 6343 ⟶wf 6512 –1-1-onto→wf1o 6515 ‘cfv 6516 (class class class)co 7391 ∈ cmpo 7393 ωcom 7841 supp csupp 8134 seq_ωcseqom 8412 +_o coa 8428 ·_o comu 8429 ↑_o coe 8430 ≈ cen 8918 finSupp cfsupp 9301 OrdIsocoi 9451 CNF ccnf 9610

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-inf2 9590

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-seqom 8413 df-1o 8431 df-2o 8432 df-oadd 8435 df-omul 8436 df-oexp 8437 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-oi 9452 df-cnf 9611

This theorem is referenced by: cnfcom2 9651 cnfcom3lem 9652 cnfcom3 9653

W3C validator