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

Theorem ptcmplem4 22660
 Description: Lemma for ptcmp 22663. (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))
ptcmplem2.5 (𝜑𝑈 ⊆ ran 𝑆)
ptcmplem2.6 (𝜑𝑋 = 𝑈)
ptcmplem2.7 (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
ptcmplem3.8 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
Assertion
Ref Expression
ptcmplem4 ¬ 𝜑
Distinct variable groups:   𝑘,𝑛,𝑢,𝑤,𝑧,𝐴   𝑢,𝐾   𝑆,𝑘,𝑛,𝑢,𝑧   𝜑,𝑘,𝑛,𝑢   𝑈,𝑘,𝑢,𝑧   𝑘,𝑉,𝑛,𝑢,𝑤,𝑧   𝑘,𝐹,𝑛,𝑢,𝑤,𝑧   𝑘,𝑋,𝑛,𝑢,𝑤,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤)   𝑆(𝑤)   𝑈(𝑤,𝑛)   𝐾(𝑧,𝑤,𝑘,𝑛)

Proof of Theorem ptcmplem4
Dummy variables 𝑓 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcmp.1 . . 3 𝑆 = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
2 ptcmp.2 . . 3 𝑋 = X𝑛𝐴 (𝐹𝑛)
3 ptcmp.3 . . 3 (𝜑𝐴𝑉)
4 ptcmp.4 . . 3 (𝜑𝐹:𝐴⟶Comp)
5 ptcmp.5 . . 3 (𝜑𝑋 ∈ (UFL ∩ dom card))
6 ptcmplem2.5 . . 3 (𝜑𝑈 ⊆ ran 𝑆)
7 ptcmplem2.6 . . 3 (𝜑𝑋 = 𝑈)
8 ptcmplem2.7 . . 3 (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9 ptcmplem3.8 . . 3 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
101, 2, 3, 4, 5, 6, 7, 8, 9ptcmplem3 22659 . 2 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
11 simprl 770 . . . . . . . . 9 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓 Fn 𝐴)
12 eldifi 4054 . . . . . . . . . . . 12 ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → (𝑓𝑘) ∈ (𝐹𝑘))
1312ralimi 3128 . . . . . . . . . . 11 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
14 fveq2 6645 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
15 fveq2 6645 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1615unieqd 4814 . . . . . . . . . . . . 13 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
1714, 16eleq12d 2884 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
1817cbvralvw 3396 . . . . . . . . . . 11 (∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛) ↔ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
1913, 18sylibr 237 . . . . . . . . . 10 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
2019ad2antll 728 . . . . . . . . 9 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
21 vex 3444 . . . . . . . . . 10 𝑓 ∈ V
2221elixp 8451 . . . . . . . . 9 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
2311, 20, 22sylanbrc 586 . . . . . . . 8 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓X𝑛𝐴 (𝐹𝑛))
2423, 2eleqtrrdi 2901 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓𝑋)
257adantr 484 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑋 = 𝑈)
2624, 25eleqtrd 2892 . . . . . 6 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓 𝑈)
27 eluni2 4804 . . . . . 6 (𝑓 𝑈 ↔ ∃𝑣𝑈 𝑓𝑣)
2826, 27sylib 221 . . . . 5 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑣𝑈 𝑓𝑣)
29 simplrr 777 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓𝑣)
3029adantr 484 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑓𝑣)
31 simprr 772 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
3230, 31eleqtrd 2892 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
33 fveq1 6644 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
3433eleq1d 2874 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
35 eqid 2798 . . . . . . . . . . . . . . . . . 18 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
3635mptpreima 6059 . . . . . . . . . . . . . . . . 17 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑢}
3734, 36elrab2 3631 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑢))
3837simprbi 500 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝑢)
3932, 38syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → (𝑓𝑘) ∈ 𝑢)
40 simprl 770 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢 ∈ (𝐹𝑘))
41 simplrl 776 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑣𝑈)
4241adantr 484 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑣𝑈)
4331, 42eqeltrrd 2891 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈)
44 rabid 3331 . . . . . . . . . . . . . . . 16 (𝑢 ∈ {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈} ↔ (𝑢 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈))
4540, 43, 44sylanbrc 586 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢 ∈ {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈})
4645, 9eleqtrrdi 2901 . . . . . . . . . . . . . 14 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢𝐾)
47 elunii 4805 . . . . . . . . . . . . . 14 (((𝑓𝑘) ∈ 𝑢𝑢𝐾) → (𝑓𝑘) ∈ 𝐾)
4839, 46, 47syl2anc 587 . . . . . . . . . . . . 13 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → (𝑓𝑘) ∈ 𝐾)
4948rexlimdvaa 3244 . . . . . . . . . . . 12 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))
5049expr 460 . . . . . . . . . . 11 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5150ralimdva 3144 . . . . . . . . . 10 (((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5251ex 416 . . . . . . . . 9 ((𝜑𝑓 Fn 𝐴) → ((𝑣𝑈𝑓𝑣) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))))
5352com23 86 . . . . . . . 8 ((𝜑𝑓 Fn 𝐴) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ((𝑣𝑈𝑓𝑣) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))))
5453impr 458 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ((𝑣𝑈𝑓𝑣) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5554imp 410 . . . . . 6 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))
566adantr 484 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑈 ⊆ ran 𝑆)
5756sselda 3915 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ 𝑣𝑈) → 𝑣 ∈ ran 𝑆)
5857adantrr 716 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → 𝑣 ∈ ran 𝑆)
591rnmpo 7263 . . . . . . . 8 ran 𝑆 = {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)}
6058, 59eleqtrdi 2900 . . . . . . 7 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → 𝑣 ∈ {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)})
61 abid 2780 . . . . . . 7 (𝑣 ∈ {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)} ↔ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
6260, 61sylib 221 . . . . . 6 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
63 rexim 3204 . . . . . 6 (∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾) → (∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾))
6455, 62, 63sylc 65 . . . . 5 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
6528, 64rexlimddv 3250 . . . 4 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
66 eldifn 4055 . . . . . . 7 ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ¬ (𝑓𝑘) ∈ 𝐾)
6766ralimi 3128 . . . . . 6 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾)
6867ad2antll 728 . . . . 5 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾)
69 ralnex 3199 . . . . 5 (∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾 ↔ ¬ ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
7068, 69sylib 221 . . . 4 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ¬ ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
7165, 70pm2.65da 816 . . 3 (𝜑 → ¬ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
7271nexdv 1937 . 2 (𝜑 → ¬ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
7310, 72pm2.65i 197 1 ¬ 𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  {crab 3110   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  𝒫 cpw 4497  ∪ cuni 4800   ↦ cmpt 5110  ◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324   ∈ cmpo 7137  Xcixp 8444  Fincfn 8492  cardccrd 9348  Compccmp 21991  UFLcufl 22505 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-omul 8090  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-fin 8496  df-wdom 9013  df-card 9352  df-acn 9355  df-cmp 21992 This theorem is referenced by:  ptcmplem5  22661
 Copyright terms: Public domain W3C validator