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

Theorem ptcmplem2 22950
Description: Lemma for ptcmp 22955. (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)𝑋 = 𝑧)
Assertion
Ref Expression
ptcmplem2 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
Distinct variable groups:   𝑘,𝑛,𝑢,𝑤,𝑧,𝐴   𝑆,𝑘,𝑛,𝑢,𝑧   𝜑,𝑘,𝑛,𝑢   𝑈,𝑘,𝑢,𝑧   𝑘,𝑉,𝑛,𝑢,𝑤,𝑧   𝑘,𝐹,𝑛,𝑢,𝑤,𝑧   𝑘,𝑋,𝑛,𝑢,𝑤,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤)   𝑆(𝑤)   𝑈(𝑤,𝑛)

Proof of Theorem ptcmplem2
Dummy variables 𝑓 𝑔 𝑚 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcmplem2.7 . . . 4 (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
2 0ss 4311 . . . . . . 7 ∅ ⊆ 𝑈
3 0fin 8849 . . . . . . 7 ∅ ∈ Fin
4 elfpw 8978 . . . . . . 7 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ⊆ 𝑈 ∧ ∅ ∈ Fin))
52, 3, 4mpbir2an 711 . . . . . 6 ∅ ∈ (𝒫 𝑈 ∩ Fin)
6 unieq 4830 . . . . . . . 8 (𝑧 = ∅ → 𝑧 = ∅)
7 uni0 4849 . . . . . . . 8 ∅ = ∅
86, 7eqtrdi 2794 . . . . . . 7 (𝑧 = ∅ → 𝑧 = ∅)
98rspceeqv 3552 . . . . . 6 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
105, 9mpan 690 . . . . 5 (𝑋 = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
1110necon3bi 2967 . . . 4 (¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧𝑋 ≠ ∅)
121, 11syl 17 . . 3 (𝜑𝑋 ≠ ∅)
13 n0 4261 . . 3 (𝑋 ≠ ∅ ↔ ∃𝑓 𝑓𝑋)
1412, 13sylib 221 . 2 (𝜑 → ∃𝑓 𝑓𝑋)
15 ptcmp.2 . . . . . . 7 𝑋 = X𝑛𝐴 (𝐹𝑛)
16 fveq2 6717 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1716unieqd 4833 . . . . . . . 8 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
1817cbvixpv 8596 . . . . . . 7 X𝑛𝐴 (𝐹𝑛) = X𝑘𝐴 (𝐹𝑘)
1915, 18eqtri 2765 . . . . . 6 𝑋 = X𝑘𝐴 (𝐹𝑘)
20 ptcmp.5 . . . . . . . 8 (𝜑𝑋 ∈ (UFL ∩ dom card))
2120elin2d 4113 . . . . . . 7 (𝜑𝑋 ∈ dom card)
2221adantr 484 . . . . . 6 ((𝜑𝑓𝑋) → 𝑋 ∈ dom card)
2319, 22eqeltrrid 2843 . . . . 5 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ∈ dom card)
24 ssrab2 3993 . . . . . 6 {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴
2512adantr 484 . . . . . . 7 ((𝜑𝑓𝑋) → 𝑋 ≠ ∅)
2619, 25eqnetrrid 3016 . . . . . 6 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ≠ ∅)
27 eqid 2737 . . . . . . 7 (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) = (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
2827resixpfo 8617 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴X𝑘𝐴 (𝐹𝑘) ≠ ∅) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
2924, 26, 28sylancr 590 . . . . 5 ((𝜑𝑓𝑋) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
30 fonum 9672 . . . . 5 ((X𝑘𝐴 (𝐹𝑘) ∈ dom card ∧ (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘)) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
3123, 29, 30syl2anc 587 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
32 vex 3412 . . . . . . . . . . 11 𝑔 ∈ V
33 difexg 5220 . . . . . . . . . . 11 (𝑔 ∈ V → (𝑔𝑓) ∈ V)
3432, 33mp1i 13 . . . . . . . . . 10 ((𝜑𝑓𝑋) → (𝑔𝑓) ∈ V)
35 dmexg 7681 . . . . . . . . . 10 ((𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
36 uniexg 7528 . . . . . . . . . 10 (dom (𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
3734, 35, 363syl 18 . . . . . . . . 9 ((𝜑𝑓𝑋) → dom (𝑔𝑓) ∈ V)
3837ralrimivw 3106 . . . . . . . 8 ((𝜑𝑓𝑋) → ∀𝑔𝑋 dom (𝑔𝑓) ∈ V)
39 eqid 2737 . . . . . . . . 9 (𝑔𝑋 dom (𝑔𝑓)) = (𝑔𝑋 dom (𝑔𝑓))
4039fnmpt 6518 . . . . . . . 8 (∀𝑔𝑋 dom (𝑔𝑓) ∈ V → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
4138, 40syl 17 . . . . . . 7 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
42 dffn4 6639 . . . . . . 7 ((𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋 ↔ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
4341, 42sylib 221 . . . . . 6 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
44 fonum 9672 . . . . . 6 ((𝑋 ∈ dom card ∧ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓))) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
4522, 43, 44syl2anc 587 . . . . 5 ((𝜑𝑓𝑋) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
46 ssdif0 4278 . . . . . . . . . . . 12 ( (𝐹𝑘) ⊆ {(𝑓𝑘)} ↔ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅)
47 simpr 488 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ⊆ {(𝑓𝑘)})
48 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → 𝑓𝑋)
4948, 19eleqtrdi 2848 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝑋) → 𝑓X𝑘𝐴 (𝐹𝑘))
50 vex 3412 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
5150elixp 8585 . . . . . . . . . . . . . . . . . . . 20 (𝑓X𝑘𝐴 (𝐹𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘)))
5251simprbi 500 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5349, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝑋) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5453r19.21bi 3130 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑓𝑘) ∈ (𝐹𝑘))
5554snssd 4722 . . . . . . . . . . . . . . . 16 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5655adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5747, 56eqssd 3918 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) = {(𝑓𝑘)})
58 fvex 6730 . . . . . . . . . . . . . . 15 (𝑓𝑘) ∈ V
5958ensn1 8694 . . . . . . . . . . . . . 14 {(𝑓𝑘)} ≈ 1o
6057, 59eqbrtrdi 5092 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ≈ 1o)
6160ex 416 . . . . . . . . . . . 12 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → ( (𝐹𝑘) ⊆ {(𝑓𝑘)} → (𝐹𝑘) ≈ 1o))
6246, 61syl5bir 246 . . . . . . . . . . 11 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ → (𝐹𝑘) ≈ 1o))
6362con3d 155 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅))
64 neq0 4260 . . . . . . . . . 10 (¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ ↔ ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}))
6563, 64syl6ib 254 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})))
66 eldifi 4041 . . . . . . . . . . . . 13 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 (𝐹𝑘))
67 simplr 769 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → 𝑥 (𝐹𝑘))
68 iftrue 4445 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = 𝑥)
6968, 17eleq12d 2832 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ 𝑥 (𝐹𝑘)))
7067, 69syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
7148, 15eleqtrdi 2848 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
7250elixp 8585 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
7372simprbi 500 . . . . . . . . . . . . . . . . . . . . 21 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7471, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7574ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7675r19.21bi 3130 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑓𝑛) ∈ (𝐹𝑛))
77 iffalse 4448 . . . . . . . . . . . . . . . . . . 19 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = (𝑓𝑛))
7877eleq1d 2822 . . . . . . . . . . . . . . . . . 18 𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ (𝑓𝑛) ∈ (𝐹𝑛)))
7976, 78syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (¬ 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8070, 79pm2.61d 182 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
8180ralrimiva 3105 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
82 ptcmp.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴𝑉)
8382ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → 𝐴𝑉)
84 mptelixpg 8616 . . . . . . . . . . . . . . . 16 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8583, 84syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8681, 85mpbird 260 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛))
8786, 15eleqtrrdi 2849 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
8866, 87sylan2 596 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
89 vex 3412 . . . . . . . . . . . . . 14 𝑘 ∈ V
9089unisn 4841 . . . . . . . . . . . . 13 {𝑘} = 𝑘
91 simplr 769 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘𝐴)
92 eleq1w 2820 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝑚𝐴𝑘𝐴))
9391, 92syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘𝑚𝐴))
9493pm4.71rd 566 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚𝐴𝑚 = 𝑘)))
95 equequ1 2033 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑛 = 𝑘𝑚 = 𝑘))
96 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9795, 96ifbieq2d 4465 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
98 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))
99 vex 3412 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
100 fvex 6730 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑚) ∈ V
10199, 100ifex 4489 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ∈ V
10297, 98, 101fvmpt 6818 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
103102neeq1d 3000 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝐴 → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
104103adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
105 iffalse 4448 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = (𝑓𝑚))
106105necon1ai 2968 . . . . . . . . . . . . . . . . . . . . 21 (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) → 𝑚 = 𝑘)
107 eldifsni 4703 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 ≠ (𝑓𝑘))
108107ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → 𝑥 ≠ (𝑓𝑘))
109 iftrue 4445 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = 𝑥)
110 fveq2 6717 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → (𝑓𝑚) = (𝑓𝑘))
111109, 110neeq12d 3002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑘 → (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) ↔ 𝑥 ≠ (𝑓𝑘)))
112108, 111syl5ibrcom 250 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
113106, 112impbid2 229 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) ↔ 𝑚 = 𝑘))
114104, 113bitrd 282 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ 𝑚 = 𝑘))
115114pm5.32da 582 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → ((𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)) ↔ (𝑚𝐴𝑚 = 𝑘)))
11694, 115bitr4d 285 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))))
117116abbidv 2807 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑚𝑚 = 𝑘} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))})
118 df-sn 4542 . . . . . . . . . . . . . . . 16 {𝑘} = {𝑚𝑚 = 𝑘}
119 df-rab 3070 . . . . . . . . . . . . . . . 16 {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))}
120117, 118, 1193eqtr4g 2803 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
121 fvex 6730 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑛) ∈ V
12299, 121ifex 4489 . . . . . . . . . . . . . . . . . 18 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
123122rgenw 3073 . . . . . . . . . . . . . . . . 17 𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
12498fnmpt 6518 . . . . . . . . . . . . . . . . 17 (∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
125123, 124mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
126 ixpfn 8584 . . . . . . . . . . . . . . . . . 18 (𝑓X𝑛𝐴 (𝐹𝑛) → 𝑓 Fn 𝐴)
12771, 126syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝑋) → 𝑓 Fn 𝐴)
128127ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑓 Fn 𝐴)
129 fndmdif 6862 . . . . . . . . . . . . . . . 16 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴𝑓 Fn 𝐴) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
130125, 128, 129syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
131120, 130eqtr4d 2780 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
132131unieqd 4833 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
13390, 132eqtr3id 2792 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
134 difeq1 4030 . . . . . . . . . . . . . . 15 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → (𝑔𝑓) = ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
135134dmeqd 5774 . . . . . . . . . . . . . 14 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
136135unieqd 4833 . . . . . . . . . . . . 13 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
137136rspceeqv 3552 . . . . . . . . . . . 12 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓)) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
13888, 133, 137syl2anc 587 . . . . . . . . . . 11 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
139138ex 416 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
140139exlimdv 1941 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14165, 140syld 47 . . . . . . . 8 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
142141expimpd 457 . . . . . . 7 ((𝜑𝑓𝑋) → ((𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14317breq1d 5063 . . . . . . . . 9 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1o (𝐹𝑘) ≈ 1o))
144143notbid 321 . . . . . . . 8 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1o ↔ ¬ (𝐹𝑘) ≈ 1o))
145144elrab 3602 . . . . . . 7 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ↔ (𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o))
14639elrnmpt 5825 . . . . . . . 8 (𝑘 ∈ V → (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
147146elv 3414 . . . . . . 7 (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
148142, 145, 1473imtr4g 299 . . . . . 6 ((𝜑𝑓𝑋) → (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} → 𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓))))
149148ssrdv 3907 . . . . 5 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓)))
150 ssnum 9653 . . . . 5 ((ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card ∧ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓))) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
15145, 149, 150syl2anc 587 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
152 xpnum 9567 . . . 4 ((X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card ∧ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card) → (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card)
15331, 151, 152syl2anc 587 . . 3 ((𝜑𝑓𝑋) → (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card)
15482adantr 484 . . . . 5 ((𝜑𝑓𝑋) → 𝐴𝑉)
155 rabexg 5224 . . . . 5 (𝐴𝑉 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
156154, 155syl 17 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
157 fvex 6730 . . . . . . 7 (𝐹𝑘) ∈ V
158157uniex 7529 . . . . . 6 (𝐹𝑘) ∈ V
159158rgenw 3073 . . . . 5 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V
160 iunexg 7736 . . . . 5 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
161156, 159, 160sylancl 589 . . . 4 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
162 resixp 8614 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴𝑓X𝑘𝐴 (𝐹𝑘)) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
16324, 49, 162sylancr 590 . . . . 5 ((𝜑𝑓𝑋) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
164163ne0d 4250 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅)
165 ixpiunwdom 9206 . . . 4 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V ∧ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
166156, 161, 164, 165syl3anc 1373 . . 3 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
167 numwdom 9673 . . 3 (((X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
168153, 166, 167syl2anc 587 . 2 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
16914, 168exlimddv 1943 1 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399   = wceq 1543  wex 1787  wcel 2110  {cab 2714  wne 2940  wral 3061  wrex 3062  {crab 3065  Vcvv 3408  cdif 3863  cin 3865  wss 3866  c0 4237  ifcif 4439  𝒫 cpw 4513  {csn 4541   cuni 4819   ciun 4904   class class class wbr 5053  cmpt 5135   × cxp 5549  ccnv 5550  dom cdm 5551  ran crn 5552  cres 5553  cima 5554   Fn wfn 6375  wf 6376  ontowfo 6378  cfv 6380  cmpo 7215  1oc1o 8195  Xcixp 8578  cen 8623  Fincfn 8626  * cwdom 9180  cardccrd 9551  Compccmp 22283  UFLcufl 22797
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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-oadd 8206  df-omul 8207  df-er 8391  df-map 8510  df-ixp 8579  df-en 8627  df-dom 8628  df-fin 8630  df-wdom 9181  df-card 9555  df-acn 9558
This theorem is referenced by:  ptcmplem3  22951
  Copyright terms: Public domain W3C validator