Theorem ptcmplem5 24043

Description: Lemma for ptcmp 24045. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypotheses

Ref	Expression
ptcmp.1	⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
ptcmp.2	⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
ptcmp.3	⊢ (𝜑 → 𝐴 ∈ 𝑉)
ptcmp.4	⊢ (𝜑 → 𝐹:𝐴⟶Comp)
ptcmp.5	⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))

Assertion

Ref	Expression
ptcmplem5	⊢ (𝜑 → (∏t‘𝐹) ∈ Comp)

Distinct variable groups:   𝑘,𝑛,𝑢,𝑤,𝐴   𝑆,𝑘,𝑛,𝑢   𝜑,𝑘,𝑛,𝑢   𝑘,𝑉,𝑛,𝑢,𝑤   𝑘,𝐹,𝑛,𝑢,𝑤   𝑘,𝑋,𝑛,𝑢,𝑤

Allowed substitution hints:   𝜑(𝑤)   𝑆(𝑤)

Proof of Theorem ptcmplem5

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcmp.5	. . 3 ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))
2	1	elin1d 4136	. 2 ⊢ (𝜑 → 𝑋 ∈ UFL)
3		ptcmp.1	. . . 4 ⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
4		ptcmp.2	. . . 4 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
5		ptcmp.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
6		ptcmp.4	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶Comp)
7	3, 4, 5, 6, 1	ptcmplem1 24039	. . 3 ⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))))
8	7	simpld 496	. 2 ⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋}))
9	7	simprd 497	. 2 ⊢ (𝜑 → (∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))))
10		elpwi 4539	. . . . . 6 ⊢ (𝑦 ∈ 𝒫 ran 𝑆 → 𝑦 ⊆ ran 𝑆)
11	5	ad2antrr 733	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐴 ∈ 𝑉)
12	6	ad2antrr 733	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐹:𝐴⟶Comp)
13	1	ad2antrr 733	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 ∈ (UFL ∩ dom card))
14		simplrl 783	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑦 ⊆ ran 𝑆)
15		simplrr 784	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 = ∪ 𝑦)
16		simpr 486	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
17		imaeq2 6015	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
18	17	eleq1d 2826	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦))
19	18	cbvrabv 3403	. . . . . . . . 9 ⊢ {𝑧 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦} = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦}
20	3, 4, 11, 12, 13, 14, 15, 16, 19	ptcmplem4 24042	. . . . . . . 8 ⊢ ¬ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
21		iman 403	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) ↔ ¬ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
22	20, 21	mpbir 233	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
23	22	expr 458	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ⊆ ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
24	10, 23	sylan2 600	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
25	24	adantlr 722	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
26		velpw 4537	. . . . . . 7 ⊢ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ↔ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋}))
27		eldif 3895	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) ↔ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆))
28		elpwunsn 4619	. . . . . . . 8 ⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦)
29	27, 28	sylbir 237	. . . . . . 7 ⊢ ((𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦)
30	26, 29	sylanbr 589	. . . . . 6 ⊢ ((𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦)
31	30	adantll 721	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦)
32		snssi 4720	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑦 → {𝑋} ⊆ 𝑦)
33	32	adantl 483	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ⊆ 𝑦)
34		snfi 8984	. . . . . . . 8 ⊢ {𝑋} ∈ Fin
35		elfpw 9258	. . . . . . . 8 ⊢ ({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ↔ ({𝑋} ⊆ 𝑦 ∧ {𝑋} ∈ Fin))
36	33, 34, 35	sylanblrc 597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ∈ (𝒫 𝑦 ∩ Fin))
37		unisng 4859	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝑦 → ∪ {𝑋} = 𝑋)
38	37	eqcomd 2747	. . . . . . . 8 ⊢ (𝑋 ∈ 𝑦 → 𝑋 = ∪ {𝑋})
39	38	adantl 483	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → 𝑋 = ∪ {𝑋})
40		unieq 4852	. . . . . . . 8 ⊢ (𝑧 = {𝑋} → ∪ 𝑧 = ∪ {𝑋})
41	40	rspceeqv 3585	. . . . . . 7 ⊢ (({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑋 = ∪ {𝑋}) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
42	36, 39, 41	syl2anc 591	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
43	42	a1d 25	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
44	31, 43	syldan 598	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
45	25, 44	pm2.61dan 819	. . 3 ⊢ ((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧))
46	45	impr 456	. 2 ⊢ ((𝜑 ∧ (𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)
47	2, 8, 9, 46	alexsub 24032	1 ⊢ (𝜑 → (∏t‘𝐹) ∈ Comp)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∃wrex 3065  {crab 3393   ∖ cdif 3882   ∪ cun 3883   ∩ cin 3884   ⊆ wss 3885  𝒫 cpw 4532  {csn 4558  ∪ cuni 4841   ↦ cmpt 5156  ^◡ccnv 5620  dom cdm 5621  ran crn 5622   “ cima 5624  ⟶wf 6485  ‘cfv 6489   ∈ cmpo 7362  Xcixp 8839  Fincfn 8887  ficfi 9317  cardccrd 9854  topGenctg 17395  ∏_tcpt 17396  Compccmp 23373  UFLcufl 23887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-oadd 8403  df-omul 8404  df-er 8637  df-map 8769  df-ixp 8840  df-en 8888  df-dom 8889  df-fin 8891  df-fi 9318  df-wdom 9474  df-card 9858  df-acn 9861  df-topgen 17401  df-pt 17402  df-fbas 21348  df-fg 21349  df-top 22881  df-topon 22898  df-bases 22933  df-cld 23006  df-ntr 23007  df-cls 23008  df-nei 23085  df-cmp 23374  df-fil 23833  df-ufil 23888  df-ufl 23889  df-flim 23926  df-fcls 23928

This theorem is referenced by:  ptcmpg  24044