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

Theorem ptcmplem4 21782
 Description: Lemma for ptcmp 21785. (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 21781 . 2 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
11 simprl 793 . . . . . . . . 9 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓 Fn 𝐴)
12 eldifi 3715 . . . . . . . . . . . 12 ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → (𝑓𝑘) ∈ (𝐹𝑘))
1312ralimi 2947 . . . . . . . . . . 11 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
14 fveq2 6153 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
15 fveq2 6153 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1615unieqd 4417 . . . . . . . . . . . . 13 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
1714, 16eleq12d 2692 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
1817cbvralv 3162 . . . . . . . . . . 11 (∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛) ↔ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
1913, 18sylibr 224 . . . . . . . . . 10 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
2019ad2antll 764 . . . . . . . . 9 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
21 vex 3192 . . . . . . . . . 10 𝑓 ∈ V
2221elixp 7867 . . . . . . . . 9 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
2311, 20, 22sylanbrc 697 . . . . . . . 8 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓X𝑛𝐴 (𝐹𝑛))
2423, 2syl6eleqr 2709 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓𝑋)
257adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑋 = 𝑈)
2624, 25eleqtrd 2700 . . . . . 6 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓 𝑈)
27 eluni2 4411 . . . . . 6 (𝑓 𝑈 ↔ ∃𝑣𝑈 𝑓𝑣)
2826, 27sylib 208 . . . . 5 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑣𝑈 𝑓𝑣)
29 simplrr 800 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑓𝑣)
3029adantr 481 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑓𝑣)
31 simprr 795 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
3230, 31eleqtrd 2700 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
33 fveq1 6152 . . . . . . . . . . . . . . . . . 18 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
3433eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑢 ↔ (𝑓𝑘) ∈ 𝑢))
35 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
3635mptpreima 5592 . . . . . . . . . . . . . . . . 17 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑢}
3734, 36elrab2 3352 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑢))
3837simprbi 480 . . . . . . . . . . . . . . 15 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝑢)
3932, 38syl 17 . . . . . . . . . . . . . 14 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → (𝑓𝑘) ∈ 𝑢)
40 simprl 793 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢 ∈ (𝐹𝑘))
41 simplrl 799 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑣𝑈)
4241adantr 481 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑣𝑈)
4331, 42eqeltrrd 2699 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈)
44 rabid 3109 . . . . . . . . . . . . . . . 16 (𝑢 ∈ {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈} ↔ (𝑢 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈))
4540, 43, 44sylanbrc 697 . . . . . . . . . . . . . . 15 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢 ∈ {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈})
4645, 9syl6eleqr 2709 . . . . . . . . . . . . . 14 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑢𝐾)
47 elunii 4412 . . . . . . . . . . . . . 14 (((𝑓𝑘) ∈ 𝑢𝑢𝐾) → (𝑓𝑘) ∈ 𝐾)
4839, 46, 47syl2anc 692 . . . . . . . . . . . . 13 (((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑢 ∈ (𝐹𝑘) ∧ 𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → (𝑓𝑘) ∈ 𝐾)
4948rexlimdvaa 3026 . . . . . . . . . . . 12 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ (𝑘𝐴 ∧ (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))
5049expr 642 . . . . . . . . . . 11 ((((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5150ralimdva 2957 . . . . . . . . . 10 (((𝜑𝑓 Fn 𝐴) ∧ (𝑣𝑈𝑓𝑣)) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5251ex 450 . . . . . . . . 9 ((𝜑𝑓 Fn 𝐴) → ((𝑣𝑈𝑓𝑣) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))))
5352com23 86 . . . . . . . 8 ((𝜑𝑓 Fn 𝐴) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ((𝑣𝑈𝑓𝑣) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))))
5453impr 648 . . . . . . 7 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ((𝑣𝑈𝑓𝑣) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾)))
5554imp 445 . . . . . 6 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾))
566adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝑈 ⊆ ran 𝑆)
5756sselda 3587 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ 𝑣𝑈) → 𝑣 ∈ ran 𝑆)
5857adantrr 752 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → 𝑣 ∈ ran 𝑆)
591rnmpt2 6730 . . . . . . . 8 ran 𝑆 = {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)}
6058, 59syl6eleq 2708 . . . . . . 7 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → 𝑣 ∈ {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)})
61 abid 2609 . . . . . . 7 (𝑣 ∈ {𝑣 ∣ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)} ↔ ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
6260, 61sylib 208 . . . . . 6 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
63 rexim 3003 . . . . . 6 (∀𝑘𝐴 (∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → (𝑓𝑘) ∈ 𝐾) → (∃𝑘𝐴𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾))
6455, 62, 63sylc 65 . . . . 5 (((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) ∧ (𝑣𝑈𝑓𝑣)) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
6528, 64rexlimddv 3029 . . . 4 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
66 eldifn 3716 . . . . . . 7 ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ¬ (𝑓𝑘) ∈ 𝐾)
6766ralimi 2947 . . . . . 6 (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾)
6867ad2antll 764 . . . . 5 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾)
69 ralnex 2987 . . . . 5 (∀𝑘𝐴 ¬ (𝑓𝑘) ∈ 𝐾 ↔ ¬ ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
7068, 69sylib 208 . . . 4 ((𝜑 ∧ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ¬ ∃𝑘𝐴 (𝑓𝑘) ∈ 𝐾)
7165, 70pm2.65da 599 . . 3 (𝜑 → ¬ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
7271nexdv 1861 . 2 (𝜑 → ¬ ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
7310, 72pm2.65i 185 1 ¬ 𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  {cab 2607  ∀wral 2907  ∃wrex 2908  {crab 2911   ∖ cdif 3556   ∩ cin 3558   ⊆ wss 3559  𝒫 cpw 4135  ∪ cuni 4407   ↦ cmpt 4678  ◡ccnv 5078  dom cdm 5079  ran crn 5080   “ cima 5082   Fn wfn 5847  ⟶wf 5848  ‘cfv 5852   ↦ cmpt2 6612  Xcixp 7860  Fincfn 7907  cardccrd 8713  Compccmp 21112  UFLcufl 21627 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-oadd 7516  df-omul 7517  df-er 7694  df-map 7811  df-ixp 7861  df-en 7908  df-dom 7909  df-fin 7911  df-wdom 8416  df-card 8717  df-acn 8720  df-cmp 21113 This theorem is referenced by:  ptcmplem5  21783
 Copyright terms: Public domain W3C validator