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

Theorem ptcmplem2 22668
 Description: Lemma for ptcmp 22673. (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 4304 . . . . . . 7 ∅ ⊆ 𝑈
3 0fin 8733 . . . . . . 7 ∅ ∈ Fin
4 elfpw 8813 . . . . . . 7 (∅ ∈ (𝒫 𝑈 ∩ Fin) ↔ (∅ ⊆ 𝑈 ∧ ∅ ∈ Fin))
52, 3, 4mpbir2an 710 . . . . . 6 ∅ ∈ (𝒫 𝑈 ∩ Fin)
6 unieq 4812 . . . . . . . 8 (𝑧 = ∅ → 𝑧 = ∅)
7 uni0 4829 . . . . . . . 8 ∅ = ∅
86, 7eqtrdi 2849 . . . . . . 7 (𝑧 = ∅ → 𝑧 = ∅)
98rspceeqv 3586 . . . . . 6 ((∅ ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∅) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
105, 9mpan 689 . . . . 5 (𝑋 = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
1110necon3bi 3013 . . . 4 (¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧𝑋 ≠ ∅)
121, 11syl 17 . . 3 (𝜑𝑋 ≠ ∅)
13 n0 4260 . . 3 (𝑋 ≠ ∅ ↔ ∃𝑓 𝑓𝑋)
1412, 13sylib 221 . 2 (𝜑 → ∃𝑓 𝑓𝑋)
15 ptcmp.2 . . . . . . 7 𝑋 = X𝑛𝐴 (𝐹𝑛)
16 fveq2 6646 . . . . . . . . 9 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1716unieqd 4815 . . . . . . . 8 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
1817cbvixpv 8465 . . . . . . 7 X𝑛𝐴 (𝐹𝑛) = X𝑘𝐴 (𝐹𝑘)
1915, 18eqtri 2821 . . . . . 6 𝑋 = X𝑘𝐴 (𝐹𝑘)
20 ptcmp.5 . . . . . . . 8 (𝜑𝑋 ∈ (UFL ∩ dom card))
2120elin2d 4126 . . . . . . 7 (𝜑𝑋 ∈ dom card)
2221adantr 484 . . . . . 6 ((𝜑𝑓𝑋) → 𝑋 ∈ dom card)
2319, 22eqeltrrid 2895 . . . . 5 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ∈ dom card)
24 ssrab2 4007 . . . . . 6 {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴
2512adantr 484 . . . . . . 7 ((𝜑𝑓𝑋) → 𝑋 ≠ ∅)
2619, 25eqnetrrid 3062 . . . . . 6 ((𝜑𝑓𝑋) → X𝑘𝐴 (𝐹𝑘) ≠ ∅)
27 eqid 2798 . . . . . . 7 (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) = (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
2827resixpfo 8486 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴X𝑘𝐴 (𝐹𝑘) ≠ ∅) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
2924, 26, 28sylancr 590 . . . . 5 ((𝜑𝑓𝑋) → (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
30 fonum 9472 . . . . 5 ((X𝑘𝐴 (𝐹𝑘) ∈ dom card ∧ (𝑔X𝑘𝐴 (𝐹𝑘) ↦ (𝑔 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})):X𝑘𝐴 (𝐹𝑘)–ontoX𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘)) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
3123, 29, 30syl2anc 587 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
32 vex 3444 . . . . . . . . . . 11 𝑔 ∈ V
33 difexg 5196 . . . . . . . . . . 11 (𝑔 ∈ V → (𝑔𝑓) ∈ V)
3432, 33mp1i 13 . . . . . . . . . 10 ((𝜑𝑓𝑋) → (𝑔𝑓) ∈ V)
35 dmexg 7597 . . . . . . . . . 10 ((𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
36 uniexg 7449 . . . . . . . . . 10 (dom (𝑔𝑓) ∈ V → dom (𝑔𝑓) ∈ V)
3734, 35, 363syl 18 . . . . . . . . 9 ((𝜑𝑓𝑋) → dom (𝑔𝑓) ∈ V)
3837ralrimivw 3150 . . . . . . . 8 ((𝜑𝑓𝑋) → ∀𝑔𝑋 dom (𝑔𝑓) ∈ V)
39 eqid 2798 . . . . . . . . 9 (𝑔𝑋 dom (𝑔𝑓)) = (𝑔𝑋 dom (𝑔𝑓))
4039fnmpt 6461 . . . . . . . 8 (∀𝑔𝑋 dom (𝑔𝑓) ∈ V → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
4138, 40syl 17 . . . . . . 7 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋)
42 dffn4 6572 . . . . . . 7 ((𝑔𝑋 dom (𝑔𝑓)) Fn 𝑋 ↔ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
4341, 42sylib 221 . . . . . 6 ((𝜑𝑓𝑋) → (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓)))
44 fonum 9472 . . . . . 6 ((𝑋 ∈ dom card ∧ (𝑔𝑋 dom (𝑔𝑓)):𝑋onto→ran (𝑔𝑋 dom (𝑔𝑓))) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
4522, 43, 44syl2anc 587 . . . . 5 ((𝜑𝑓𝑋) → ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card)
46 ssdif0 4277 . . . . . . . . . . . 12 ( (𝐹𝑘) ⊆ {(𝑓𝑘)} ↔ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅)
47 simpr 488 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ⊆ {(𝑓𝑘)})
48 simpr 488 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → 𝑓𝑋)
4948, 19eleqtrdi 2900 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑓𝑋) → 𝑓X𝑘𝐴 (𝐹𝑘))
50 vex 3444 . . . . . . . . . . . . . . . . . . . . 21 𝑓 ∈ V
5150elixp 8454 . . . . . . . . . . . . . . . . . . . 20 (𝑓X𝑘𝐴 (𝐹𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘)))
5251simprbi 500 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝐴 (𝐹𝑘) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5349, 52syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑓𝑋) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝐹𝑘))
5453r19.21bi 3173 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑓𝑘) ∈ (𝐹𝑘))
5554snssd 4702 . . . . . . . . . . . . . . . 16 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5655adantr 484 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → {(𝑓𝑘)} ⊆ (𝐹𝑘))
5747, 56eqssd 3932 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) = {(𝑓𝑘)})
58 fvex 6659 . . . . . . . . . . . . . . 15 (𝑓𝑘) ∈ V
5958ensn1 8559 . . . . . . . . . . . . . 14 {(𝑓𝑘)} ≈ 1o
6057, 59eqbrtrdi 5070 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ (𝐹𝑘) ⊆ {(𝑓𝑘)}) → (𝐹𝑘) ≈ 1o)
6160ex 416 . . . . . . . . . . . 12 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → ( (𝐹𝑘) ⊆ {(𝑓𝑘)} → (𝐹𝑘) ≈ 1o))
6246, 61syl5bir 246 . . . . . . . . . . 11 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ → (𝐹𝑘) ≈ 1o))
6362con3d 155 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅))
64 neq0 4259 . . . . . . . . . 10 (¬ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) = ∅ ↔ ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}))
6563, 64syl6ib 254 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})))
66 eldifi 4054 . . . . . . . . . . . . 13 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 (𝐹𝑘))
67 simplr 768 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → 𝑥 (𝐹𝑘))
68 iftrue 4431 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = 𝑥)
6968, 17eleq12d 2884 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ 𝑥 (𝐹𝑘)))
7067, 69syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
7148, 15eleqtrdi 2900 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
7250elixp 8454 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
7372simprbi 500 . . . . . . . . . . . . . . . . . . . . 21 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7471, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7574ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
7675r19.21bi 3173 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (𝑓𝑛) ∈ (𝐹𝑛))
77 iffalse 4434 . . . . . . . . . . . . . . . . . . 19 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = (𝑓𝑛))
7877eleq1d 2874 . . . . . . . . . . . . . . . . . 18 𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛) ↔ (𝑓𝑛) ∈ (𝐹𝑛)))
7976, 78syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → (¬ 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8070, 79pm2.61d 182 . . . . . . . . . . . . . . . 16 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) ∧ 𝑛𝐴) → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
8180ralrimiva 3149 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛))
82 ptcmp.3 . . . . . . . . . . . . . . . . 17 (𝜑𝐴𝑉)
8382ad3antrrr 729 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → 𝐴𝑉)
84 mptelixpg 8485 . . . . . . . . . . . . . . . 16 (𝐴𝑉 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8583, 84syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛) ↔ ∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ (𝐹𝑛)))
8681, 85mpbird 260 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ X𝑛𝐴 (𝐹𝑛))
8786, 15eleqtrrdi 2901 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 (𝐹𝑘)) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
8866, 87sylan2 595 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋)
89 vex 3444 . . . . . . . . . . . . . 14 𝑘 ∈ V
9089unisn 4821 . . . . . . . . . . . . 13 {𝑘} = 𝑘
91 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘𝐴)
92 eleq1w 2872 . . . . . . . . . . . . . . . . . . . 20 (𝑚 = 𝑘 → (𝑚𝐴𝑘𝐴))
9391, 92syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘𝑚𝐴))
9493pm4.71rd 566 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚𝐴𝑚 = 𝑘)))
95 equequ1 2032 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑛 = 𝑘𝑚 = 𝑘))
96 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑚 → (𝑓𝑛) = (𝑓𝑚))
9795, 96ifbieq2d 4450 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑚 → if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
98 eqid 2798 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))
99 vex 3444 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑥 ∈ V
100 fvex 6659 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓𝑚) ∈ V
10199, 100ifex 4473 . . . . . . . . . . . . . . . . . . . . . . 23 if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ∈ V
10297, 98, 101fvmpt 6746 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚𝐴 → ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) = if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)))
103102neeq1d 3046 . . . . . . . . . . . . . . . . . . . . 21 (𝑚𝐴 → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
104103adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚)))
105 iffalse 4434 . . . . . . . . . . . . . . . . . . . . . 22 𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = (𝑓𝑚))
106105necon1ai 3014 . . . . . . . . . . . . . . . . . . . . 21 (if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) ≠ (𝑓𝑚) → 𝑚 = 𝑘)
107 eldifsni 4683 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → 𝑥 ≠ (𝑓𝑘))
108107ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) ∧ 𝑚𝐴) → 𝑥 ≠ (𝑓𝑘))
109 iftrue 4431 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓𝑚)) = 𝑥)
110 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 = 𝑘 → (𝑓𝑚) = (𝑓𝑘))
111109, 110neeq12d 3048 . . . . . . . . . . . . . . . . . . . . . 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 2862 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑚𝑚 = 𝑘} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))})
118 df-sn 4526 . . . . . . . . . . . . . . . 16 {𝑘} = {𝑚𝑚 = 𝑘}
119 df-rab 3115 . . . . . . . . . . . . . . . 16 {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)} = {𝑚 ∣ (𝑚𝐴 ∧ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚))}
120117, 118, 1193eqtr4g 2858 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
121 fvex 6659 . . . . . . . . . . . . . . . . . . 19 (𝑓𝑛) ∈ V
12299, 121ifex 4473 . . . . . . . . . . . . . . . . . 18 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
123122rgenw 3118 . . . . . . . . . . . . . . . . 17 𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V
12498fnmpt 6461 . . . . . . . . . . . . . . . . 17 (∀𝑛𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)) ∈ V → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
125123, 124mp1i 13 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴)
126 ixpfn 8453 . . . . . . . . . . . . . . . . . 18 (𝑓X𝑛𝐴 (𝐹𝑛) → 𝑓 Fn 𝐴)
12771, 126syl 17 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓𝑋) → 𝑓 Fn 𝐴)
128127ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑓 Fn 𝐴)
129 fndmdif 6790 . . . . . . . . . . . . . . . 16 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) Fn 𝐴𝑓 Fn 𝐴) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
130125, 128, 129syl2anc 587 . . . . . . . . . . . . . . 15 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓) = {𝑚𝐴 ∣ ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛)))‘𝑚) ≠ (𝑓𝑚)})
131120, 130eqtr4d 2836 . . . . . . . . . . . . . 14 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
132131unieqd 4815 . . . . . . . . . . . . 13 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → {𝑘} = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
13390, 132syl5eqr 2847 . . . . . . . . . . . 12 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → 𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
134 difeq1 4043 . . . . . . . . . . . . . . 15 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → (𝑔𝑓) = ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
135134dmeqd 5739 . . . . . . . . . . . . . 14 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
136135unieqd 4815 . . . . . . . . . . . . 13 (𝑔 = (𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) → dom (𝑔𝑓) = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓))
137136rspceeqv 3586 . . . . . . . . . . . 12 (((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∈ 𝑋𝑘 = dom ((𝑛𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓𝑛))) ∖ 𝑓)) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
13888, 133, 137syl2anc 587 . . . . . . . . . . 11 ((((𝜑𝑓𝑋) ∧ 𝑘𝐴) ∧ 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)})) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
139138ex 416 . . . . . . . . . 10 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
140139exlimdv 1934 . . . . . . . . 9 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (∃𝑥 𝑥 ∈ ( (𝐹𝑘) ∖ {(𝑓𝑘)}) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14165, 140syld 47 . . . . . . . 8 (((𝜑𝑓𝑋) ∧ 𝑘𝐴) → (¬ (𝐹𝑘) ≈ 1o → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
142141expimpd 457 . . . . . . 7 ((𝜑𝑓𝑋) → ((𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o) → ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
14317breq1d 5041 . . . . . . . . 9 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1o (𝐹𝑘) ≈ 1o))
144143notbid 321 . . . . . . . 8 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1o ↔ ¬ (𝐹𝑘) ≈ 1o))
145144elrab 3628 . . . . . . 7 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ↔ (𝑘𝐴 ∧ ¬ (𝐹𝑘) ≈ 1o))
14639elrnmpt 5793 . . . . . . . 8 (𝑘 ∈ V → (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓)))
147146elv 3446 . . . . . . 7 (𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓)) ↔ ∃𝑔𝑋 𝑘 = dom (𝑔𝑓))
148142, 145, 1473imtr4g 299 . . . . . 6 ((𝜑𝑓𝑋) → (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} → 𝑘 ∈ ran (𝑔𝑋 dom (𝑔𝑓))))
149148ssrdv 3921 . . . . 5 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓)))
150 ssnum 9453 . . . . 5 ((ran (𝑔𝑋 dom (𝑔𝑓)) ∈ dom card ∧ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ ran (𝑔𝑋 dom (𝑔𝑓))) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
15145, 149, 150syl2anc 587 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ dom card)
152 xpnum 9367 . . . 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 5199 . . . . 5 (𝐴𝑉 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
156154, 155syl 17 . . . 4 ((𝜑𝑓𝑋) → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
157 fvex 6659 . . . . . . 7 (𝐹𝑘) ∈ V
158157uniex 7450 . . . . . 6 (𝐹𝑘) ∈ V
159158rgenw 3118 . . . . 5 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V
160 iunexg 7649 . . . . 5 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
161156, 159, 160sylancl 589 . . . 4 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V)
162 resixp 8483 . . . . . 6 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ⊆ 𝐴𝑓X𝑘𝐴 (𝐹𝑘)) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
16324, 49, 162sylancr 590 . . . . 5 ((𝜑𝑓𝑋) → (𝑓 ↾ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
164163ne0d 4251 . . . 4 ((𝜑𝑓𝑋) → X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅)
165 ixpiunwdom 9041 . . . 4 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ V ∧ X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≠ ∅) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
166156, 161, 164, 165syl3anc 1368 . . 3 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}))
167 numwdom 9473 . . 3 (((X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ≼* (X𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) × {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o})) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
168153, 166, 167syl2anc 587 . 2 ((𝜑𝑓𝑋) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
16914, 168exlimddv 1936 1 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425  𝒫 cpw 4497  {csn 4525  ∪ cuni 4801  ∪ ciun 4882   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  ◡ccnv 5519  dom cdm 5520  ran crn 5521   ↾ cres 5522   “ cima 5523   Fn wfn 6320  ⟶wf 6321  –onto→wfo 6323  ‘cfv 6325   ∈ cmpo 7138  1oc1o 8081  Xcixp 8447   ≈ cen 8492  Fincfn 8495   ≼* cwdom 9015  cardccrd 9351  Compccmp 22001  UFLcufl 22515 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 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 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 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-se 5480  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-isom 6334  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-oadd 8092  df-omul 8093  df-er 8275  df-map 8394  df-ixp 8448  df-en 8496  df-dom 8497  df-fin 8499  df-wdom 9016  df-card 9355  df-acn 9358 This theorem is referenced by:  ptcmplem3  22669
 Copyright terms: Public domain W3C validator