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

Theorem ptcmplem2 24061
Description: Lemma for ptcmp 24066. (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 4400 . . . . . . 7 ∅ ⊆ 𝑈
3 0fi 9082 . . . . . . 7 ∅ ∈ Fin
4 elfpw 9394 . . . . . . 7 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ⊆ 𝑈 ∧ ∅ ∈ Fin))
52, 3, 4mpbir2an 711 . . . . . 6 ∅ ∈ (𝒫 𝑈 ∩ Fin)
6 unieq 4918 . . . . . . . 8 (𝑧 = ∅ → 𝑧 = ∅)
7 uni0 4935 . . . . . . . 8 ∅ = ∅
86, 7eqtrdi 2793 . . . . . . 7 (𝑧 = ∅ → 𝑧 = ∅)
98rspceeqv 3645 . . . . . 6 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
105, 9mpan 690 . . . . 5 (𝑋 = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
1110necon3bi 2967 . . . 4 (¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧𝑋 ≠ ∅)
121, 11syl 17 . . 3 (𝜑𝑋 ≠ ∅)
13 n0 4353 . . 3 (𝑋 ≠ ∅ ↔ ∃𝑓 𝑓𝑋)
1412, 13sylib 218 . 2 (𝜑 → ∃𝑓 𝑓𝑋)
15 ptcmp.2 . . . . . . 7 𝑋 = X𝑛𝐴 (𝐹𝑛)
16 fveq2 6906 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1716unieqd 4920 . . . . . . . 8 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
1817cbvixpv 8955 . . . . . . 7 X𝑛𝐴 (𝐹𝑛) = X𝑘𝐴 (𝐹𝑘)
1915, 18eqtri 2765 . . . . . 6 𝑋 = X𝑘𝐴 (𝐹𝑘)
20 ptcmp.5 . . . . . . . 8 (𝜑𝑋 ∈ (UFL ∩ dom card))
2120elin2d 4205 . . . . . . 7 (𝜑𝑋 ∈ dom card)
2221adantr 480 . . . . . 6 ((𝜑𝑓𝑋) → 𝑋 ∈ dom card)
2319, 22eqeltrrid 2846 . . . . 5 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ∈ dom card)
24 ssrab2 4080 . . . . . 6 {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴
2512adantr 480 . . . . . . 7 ((𝜑𝑓𝑋) → 𝑋 ≠ ∅)
2619, 25eqnetrrid 3016 . . . . . 6 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ≠ ∅)
27 eqid 2737 . . . . . . 7 (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) = (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
2827resixpfo 8976 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴X𝑘𝐴 (𝐹𝑘) ≠ ∅) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
2924, 26, 28sylancr 587 . . . . 5 ((𝜑𝑓𝑋) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
30 fonum 10098 . . . . 5 ((X𝑘𝐴 (𝐹𝑘) ∈ dom card ∧ (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘)) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
3123, 29, 30syl2anc 584 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
32 vex 3484 . . . . . . . . . . 11 𝑔 ∈ V
33 difexg 5329 . . . . . . . . . . 11 (𝑔 ∈ V → (𝑔𝑓) ∈ V)
3432, 33mp1i 13 . . . . . . . . . 10 ((𝜑𝑓𝑋) → (𝑔𝑓) ∈ V)
35 dmexg 7923 . . . . . . . . . 10 ((𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
36 uniexg 7760 . . . . . . . . . 10 (dom (𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
3734, 35, 363syl 18 . . . . . . . . 9 ((𝜑𝑓𝑋) → dom (𝑔𝑓) ∈ V)
3837ralrimivw 3150 . . . . . . . 8 ((𝜑𝑓𝑋) → ∀𝑔𝑋 dom (𝑔𝑓) ∈ V)
39 eqid 2737 . . . . . . . . 9 (𝑔𝑋 dom (𝑔𝑓)) = (𝑔𝑋 dom (𝑔𝑓))
4039fnmpt 6708 . . . . . . . 8 (∀𝑔𝑋 dom (𝑔𝑓) ∈ V → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
4138, 40syl 17 . . . . . . 7 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
42 dffn4 6826 . . . . . . 7 ((𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋 ↔ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
4341, 42sylib 218 . . . . . 6 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
44 fonum 10098 . . . . . 6 ((𝑋 ∈ dom card ∧ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓))) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
4522, 43, 44syl2anc 584 . . . . 5 ((𝜑𝑓𝑋) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
46 ssdif0 4366 . . . . . . . . . . . 12 ( (𝐹𝑘) ⊆ {(𝑓𝑘)} ↔ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅)
47 simpr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ⊆ {(𝑓𝑘)})
48 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → 𝑓𝑋)
4948, 19eleqtrdi 2851 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝑋) → 𝑓X𝑘𝐴 (𝐹𝑘))
50 vex 3484 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
5150elixp 8944 . . . . . . . . . . . . . . . . . . . 20 (𝑓X𝑘𝐴 (𝐹𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘)))
5251simprbi 496 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5349, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝑋) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5453r19.21bi 3251 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑓𝑘) ∈ (𝐹𝑘))
5554snssd 4809 . . . . . . . . . . . . . . . 16 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5655adantr 480 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5747, 56eqssd 4001 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) = {(𝑓𝑘)})
58 fvex 6919 . . . . . . . . . . . . . . 15 (𝑓𝑘) ∈ V
5958ensn1 9061 . . . . . . . . . . . . . 14 {(𝑓𝑘)} ≈ 1o
6057, 59eqbrtrdi 5182 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ≈ 1o)
6160ex 412 . . . . . . . . . . . 12 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → ( (𝐹𝑘) ⊆ {(𝑓𝑘)} → (𝐹𝑘) ≈ 1o))
6246, 61biimtrrid 243 . . . . . . . . . . 11 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ → (𝐹𝑘) ≈ 1o))
6362con3d 152 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅))
64 neq0 4352 . . . . . . . . . 10 (¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ ↔ ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}))
6563, 64imbitrdi 251 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})))
66 eldifi 4131 . . . . . . . . . . . . 13 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 (𝐹𝑘))
67 simplr 769 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → 𝑥 (𝐹𝑘))
68 iftrue 4531 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = 𝑥)
6968, 17eleq12d 2835 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ 𝑥 (𝐹𝑘)))
7067, 69syl5ibrcom 247 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
7148, 15eleqtrdi 2851 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
7250elixp 8944 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
7372simprbi 496 . . . . . . . . . . . . . . . . . . . . 21 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7471, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7574ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7675r19.21bi 3251 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑓𝑛) ∈ (𝐹𝑛))
77 iffalse 4534 . . . . . . . . . . . . . . . . . . 19 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = (𝑓𝑛))
7877eleq1d 2826 . . . . . . . . . . . . . . . . . 18 𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ (𝑓𝑛) ∈ (𝐹𝑛)))
7976, 78syl5ibrcom 247 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (¬ 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8070, 79pm2.61d 179 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
8180ralrimiva 3146 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
82 ptcmp.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴𝑉)
8382ad3antrrr 730 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → 𝐴𝑉)
84 mptelixpg 8975 . . . . . . . . . . . . . . . 16 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8583, 84syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8681, 85mpbird 257 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛))
8786, 15eleqtrrdi 2852 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
8866, 87sylan2 593 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
89 unisnv 4927 . . . . . . . . . . . . 13 {𝑘} = 𝑘
90 simplr 769 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘𝐴)
91 eleq1w 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝑚𝐴𝑘𝐴))
9290, 91syl5ibrcom 247 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘𝑚𝐴))
9392pm4.71rd 562 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚𝐴𝑚 = 𝑘)))
94 equequ1 2024 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑛 = 𝑘𝑚 = 𝑘))
95 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9694, 95ifbieq2d 4552 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
97 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))
98 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
99 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑚) ∈ V
10098, 99ifex 4576 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ∈ V
10196, 97, 100fvmpt 7016 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
102101neeq1d 3000 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝐴 → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
103102adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
104 iffalse 4534 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = (𝑓𝑚))
105104necon1ai 2968 . . . . . . . . . . . . . . . . . . . . 21 (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) → 𝑚 = 𝑘)
106 eldifsni 4790 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 ≠ (𝑓𝑘))
107106ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → 𝑥 ≠ (𝑓𝑘))
108 iftrue 4531 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = 𝑥)
109 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → (𝑓𝑚) = (𝑓𝑘))
110108, 109neeq12d 3002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 = 𝑘 → (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) ↔ 𝑥 ≠ (𝑓𝑘)))
111107, 110syl5ibrcom 247 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
112105, 111impbid2 226 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) ↔ 𝑚 = 𝑘))
113103, 112bitrd 279 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ 𝑚 = 𝑘))
114113pm5.32da 579 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → ((𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)) ↔ (𝑚𝐴𝑚 = 𝑘)))
11593, 114bitr4d 282 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))))
116115abbidv 2808 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑚𝑚 = 𝑘} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))})
117 df-sn 4627 . . . . . . . . . . . . . . . 16 {𝑘} = {𝑚𝑚 = 𝑘}
118 df-rab 3437 . . . . . . . . . . . . . . . 16 {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))}
119116, 117, 1183eqtr4g 2802 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
120 fvex 6919 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑛) ∈ V
12198, 120ifex 4576 . . . . . . . . . . . . . . . . . 18 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
122121rgenw 3065 . . . . . . . . . . . . . . . . 17 𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
12397fnmpt 6708 . . . . . . . . . . . . . . . . 17 (∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
124122, 123mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
125 ixpfn 8943 . . . . . . . . . . . . . . . . . 18 (𝑓X𝑛𝐴 (𝐹𝑛) → 𝑓 Fn 𝐴)
12671, 125syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝑋) → 𝑓 Fn 𝐴)
127126ad2antrr 726 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑓 Fn 𝐴)
128 fndmdif 7062 . . . . . . . . . . . . . . . 16 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴𝑓 Fn 𝐴) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
129124, 127, 128syl2anc 584 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
130119, 129eqtr4d 2780 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
131130unieqd 4920 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
13289, 131eqtr3id 2791 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
133 difeq1 4119 . . . . . . . . . . . . . . 15 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → (𝑔𝑓) = ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
134133dmeqd 5916 . . . . . . . . . . . . . 14 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
135134unieqd 4920 . . . . . . . . . . . . 13 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
136135rspceeqv 3645 . . . . . . . . . . . 12 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓)) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
13788, 132, 136syl2anc 584 . . . . . . . . . . 11 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
138137ex 412 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
139138exlimdv 1933 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14065, 139syld 47 . . . . . . . 8 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
141140expimpd 453 . . . . . . 7 ((𝜑𝑓𝑋) → ((𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14217breq1d 5153 . . . . . . . . 9 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1o (𝐹𝑘) ≈ 1o))
143142notbid 318 . . . . . . . 8 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1o ↔ ¬ (𝐹𝑘) ≈ 1o))
144143elrab 3692 . . . . . . 7 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ↔ (𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o))
14539elrnmpt 5969 . . . . . . . 8 (𝑘 ∈ V → (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
146145elv 3485 . . . . . . 7 (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
147141, 144, 1463imtr4g 296 . . . . . 6 ((𝜑𝑓𝑋) → (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} → 𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓))))
148147ssrdv 3989 . . . . 5 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓)))
149 ssnum 10079 . . . . 5 ((ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card ∧ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓))) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
15045, 148, 149syl2anc 584 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
151 xpnum 9991 . . . 4 ((X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card ∧ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card) → (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card)
15231, 150, 151syl2anc 584 . . 3 ((𝜑𝑓𝑋) → (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card)
15382adantr 480 . . . . 5 ((𝜑𝑓𝑋) → 𝐴𝑉)
154 rabexg 5337 . . . . 5 (𝐴𝑉 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
155153, 154syl 17 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
156 fvex 6919 . . . . . . 7 (𝐹𝑘) ∈ V
157156uniex 7761 . . . . . 6 (𝐹𝑘) ∈ V
158157rgenw 3065 . . . . 5 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V
159 iunexg 7988 . . . . 5 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
160155, 158, 159sylancl 586 . . . 4 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
161 resixp 8973 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴𝑓X𝑘𝐴 (𝐹𝑘)) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
16224, 49, 161sylancr 587 . . . . 5 ((𝜑𝑓𝑋) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
163162ne0d 4342 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅)
164 ixpiunwdom 9630 . . . 4 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V ∧ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
165155, 160, 163, 164syl3anc 1373 . . 3 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
166 numwdom 10099 . . 3 (((X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
167152, 165, 166syl2anc 584 . 2 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
16814, 167exlimddv 1935 1 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626   cuni 4907   ciun 4991   class class class wbr 5143  cmpt 5225   × cxp 5683  ccnv 5684  dom cdm 5685  ran crn 5686  cres 5687  cima 5688   Fn wfn 6556  wf 6557  ontowfo 6559  cfv 6561  cmpo 7433  1oc1o 8499  Xcixp 8937  cen 8982  Fincfn 8985  * cwdom 9604  cardccrd 9975  Compccmp 23394  UFLcufl 23908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-omul 8511  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-fin 8989  df-wdom 9605  df-card 9979  df-acn 9982
This theorem is referenced by:  ptcmplem3  24062
  Copyright terms: Public domain W3C validator