Step | Hyp | Ref
| Expression |
1 | | ptcmplem2.7 |
. . . 4
⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
2 | | 0ss 4356 |
. . . . . . 7
⊢ ∅
⊆ 𝑈 |
3 | | 0fin 9115 |
. . . . . . 7
⊢ ∅
∈ Fin |
4 | | elfpw 9298 |
. . . . . . 7
⊢ (∅
∈ (𝒫 𝑈 ∩
Fin) ↔ (∅ ⊆ 𝑈 ∧ ∅ ∈ Fin)) |
5 | 2, 3, 4 | mpbir2an 709 |
. . . . . 6
⊢ ∅
∈ (𝒫 𝑈 ∩
Fin) |
6 | | unieq 4876 |
. . . . . . . 8
⊢ (𝑧 = ∅ → ∪ 𝑧 =
∪ ∅) |
7 | | uni0 4896 |
. . . . . . . 8
⊢ ∪ ∅ = ∅ |
8 | 6, 7 | eqtrdi 2792 |
. . . . . . 7
⊢ (𝑧 = ∅ → ∪ 𝑧 =
∅) |
9 | 8 | rspceeqv 3595 |
. . . . . 6
⊢ ((∅
∈ (𝒫 𝑈 ∩
Fin) ∧ 𝑋 = ∅)
→ ∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)𝑋 = ∪ 𝑧) |
10 | 5, 9 | mpan 688 |
. . . . 5
⊢ (𝑋 = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) |
11 | 10 | necon3bi 2970 |
. . . 4
⊢ (¬
∃𝑧 ∈ (𝒫
𝑈 ∩ Fin)𝑋 = ∪
𝑧 → 𝑋 ≠ ∅) |
12 | 1, 11 | syl 17 |
. . 3
⊢ (𝜑 → 𝑋 ≠ ∅) |
13 | | n0 4306 |
. . 3
⊢ (𝑋 ≠ ∅ ↔
∃𝑓 𝑓 ∈ 𝑋) |
14 | 12, 13 | sylib 217 |
. 2
⊢ (𝜑 → ∃𝑓 𝑓 ∈ 𝑋) |
15 | | ptcmp.2 |
. . . . . . 7
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
16 | | fveq2 6842 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) |
17 | 16 | unieqd 4879 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘)) |
18 | 17 | cbvixpv 8853 |
. . . . . . 7
⊢ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) |
19 | 15, 18 | eqtri 2764 |
. . . . . 6
⊢ 𝑋 = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) |
20 | | ptcmp.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
21 | 20 | elin2d 4159 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ dom card) |
22 | 21 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ∈ dom card) |
23 | 19, 22 | eqeltrrid 2843 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ dom card) |
24 | | ssrab2 4037 |
. . . . . 6
⊢ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 |
25 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ≠ ∅) |
26 | 19, 25 | eqnetrrid 3019 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ≠ ∅) |
27 | | eqid 2736 |
. . . . . . 7
⊢ (𝑔 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) = (𝑔 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) |
28 | 27 | resixpfo 8874 |
. . . . . 6
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 ∧ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ≠ ∅) → (𝑔 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})):X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘)–onto→X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
29 | 24, 26, 28 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})):X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘)–onto→X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
30 | | fonum 9994 |
. . . . 5
⊢ ((X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ∈ dom card ∧ (𝑔 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})):X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘)–onto→X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |
31 | 23, 29, 30 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |
32 | | vex 3449 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
33 | | difexg 5284 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ V → (𝑔 ∖ 𝑓) ∈ V) |
34 | 32, 33 | mp1i 13 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∖ 𝑓) ∈ V) |
35 | | dmexg 7840 |
. . . . . . . . . 10
⊢ ((𝑔 ∖ 𝑓) ∈ V → dom (𝑔 ∖ 𝑓) ∈ V) |
36 | | uniexg 7677 |
. . . . . . . . . 10
⊢ (dom
(𝑔 ∖ 𝑓) ∈ V → ∪ dom (𝑔 ∖ 𝑓) ∈ V) |
37 | 34, 35, 36 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪ dom
(𝑔 ∖ 𝑓) ∈ V) |
38 | 37 | ralrimivw 3147 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑔 ∈ 𝑋 ∪ dom (𝑔 ∖ 𝑓) ∈ V) |
39 | | eqid 2736 |
. . . . . . . . 9
⊢ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) = (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) |
40 | 39 | fnmpt 6641 |
. . . . . . . 8
⊢
(∀𝑔 ∈
𝑋 ∪ dom (𝑔 ∖ 𝑓) ∈ V → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋) |
41 | 38, 40 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋) |
42 | | dffn4 6762 |
. . . . . . 7
⊢ ((𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋 ↔ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) |
43 | 41, 42 | sylib 217 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) |
44 | | fonum 9994 |
. . . . . 6
⊢ ((𝑋 ∈ dom card ∧ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) → ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom
card) |
45 | 22, 43, 44 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom
card) |
46 | | ssdif0 4323 |
. . . . . . . . . . . 12
⊢ (∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)} ↔ (∪
(𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅) |
47 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) |
48 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) |
49 | 48, 19 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) |
50 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑓 ∈ V |
51 | 50 | elixp 8842 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))) |
52 | 51 | simprbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
53 | 49, 52 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
54 | 53 | r19.21bi 3234 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) |
55 | 54 | snssd 4769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → {(𝑓‘𝑘)} ⊆ ∪
(𝐹‘𝑘)) |
56 | 55 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → {(𝑓‘𝑘)} ⊆ ∪
(𝐹‘𝑘)) |
57 | 47, 56 | eqssd 3961 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) = {(𝑓‘𝑘)}) |
58 | | fvex 6855 |
. . . . . . . . . . . . . . 15
⊢ (𝑓‘𝑘) ∈ V |
59 | 58 | ensn1 8961 |
. . . . . . . . . . . . . 14
⊢ {(𝑓‘𝑘)} ≈ 1o |
60 | 57, 59 | eqbrtrdi 5144 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) ≈ 1o) |
61 | 60 | ex 413 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ⊆ {(𝑓‘𝑘)} → ∪ (𝐹‘𝑘) ≈ 1o)) |
62 | 46, 61 | biimtrrid 242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → ((∪
(𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅ → ∪ (𝐹‘𝑘) ≈ 1o)) |
63 | 62 | con3d 152 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ¬ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅)) |
64 | | neq0 4305 |
. . . . . . . . . 10
⊢ (¬
(∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅ ↔ ∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) |
65 | 63, 64 | syl6ib 250 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}))) |
66 | | eldifi 4086 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → 𝑥 ∈ ∪ (𝐹‘𝑘)) |
67 | | simplr 767 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → 𝑥 ∈ ∪ (𝐹‘𝑘)) |
68 | | iftrue 4492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = 𝑥) |
69 | 68, 17 | eleq12d 2832 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛) ↔ 𝑥 ∈ ∪ (𝐹‘𝑘))) |
70 | 67, 69 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) |
71 | 48, 15 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) |
72 | 50 | elixp 8842 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) |
73 | 72 | simprbi 497 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
74 | 71, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
75 | 74 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
76 | 75 | r19.21bi 3234 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) |
77 | | iffalse 4495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = (𝑓‘𝑛)) |
78 | 77 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) |
79 | 76, 78 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (¬ 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) |
80 | 70, 79 | pm2.61d 179 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛)) |
81 | 80 | ralrimiva 3143 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛)) |
82 | | ptcmp.3 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
83 | 82 | ad3antrrr 728 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → 𝐴 ∈ 𝑉) |
84 | | mptelixpg 8873 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) |
86 | 81, 85 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) |
87 | 86, 15 | eleqtrrdi 2849 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋) |
88 | 66, 87 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋) |
89 | | unisnv 4888 |
. . . . . . . . . . . . 13
⊢ ∪ {𝑘}
= 𝑘 |
90 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑘 ∈ 𝐴) |
91 | | eleq1w 2820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑘 → (𝑚 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) |
92 | 90, 91 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 → 𝑚 ∈ 𝐴)) |
93 | 92 | pm4.71rd 563 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘))) |
94 | | equequ1 2028 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑛 = 𝑘 ↔ 𝑚 = 𝑘)) |
95 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) |
96 | 94, 95 | ifbieq2d 4512 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚))) |
97 | | eqid 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) |
98 | | vex 3449 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑥 ∈ V |
99 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓‘𝑚) ∈ V |
100 | 98, 99 | ifex 4536 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ∈ V |
101 | 96, 97, 100 | fvmpt 6948 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ 𝐴 → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) = if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚))) |
102 | 101 | neeq1d 3003 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ 𝐴 → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) |
103 | 102 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) |
104 | | iffalse 4495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) = (𝑓‘𝑚)) |
105 | 104 | necon1ai 2971 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) → 𝑚 = 𝑘) |
106 | | eldifsni 4750 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → 𝑥 ≠ (𝑓‘𝑘)) |
107 | 106 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → 𝑥 ≠ (𝑓‘𝑘)) |
108 | | iftrue 4492 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) = 𝑥) |
109 | | fveq2 6842 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑘 → (𝑓‘𝑚) = (𝑓‘𝑘)) |
110 | 108, 109 | neeq12d 3005 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑘 → (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) ↔ 𝑥 ≠ (𝑓‘𝑘))) |
111 | 107, 110 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) |
112 | 105, 111 | impbid2 225 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) ↔ 𝑚 = 𝑘)) |
113 | 103, 112 | bitrd 278 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ 𝑚 = 𝑘)) |
114 | 113 | pm5.32da 579 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ((𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)) ↔ (𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘))) |
115 | 93, 114 | bitr4d 281 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)))) |
116 | 115 | abbidv 2805 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑚 ∣ 𝑚 = 𝑘} = {𝑚 ∣ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚))}) |
117 | | df-sn 4587 |
. . . . . . . . . . . . . . . 16
⊢ {𝑘} = {𝑚 ∣ 𝑚 = 𝑘} |
118 | | df-rab 3408 |
. . . . . . . . . . . . . . . 16
⊢ {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)} = {𝑚 ∣ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚))} |
119 | 116, 117,
118 | 3eqtr4g 2801 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑘} = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) |
120 | | fvex 6855 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓‘𝑛) ∈ V |
121 | 98, 120 | ifex 4536 |
. . . . . . . . . . . . . . . . . 18
⊢ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V |
122 | 121 | rgenw 3068 |
. . . . . . . . . . . . . . . . 17
⊢
∀𝑛 ∈
𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V |
123 | 97 | fnmpt 6641 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴) |
125 | | ixpfn 8841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → 𝑓 Fn 𝐴) |
126 | 71, 125 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐴) |
127 | 126 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑓 Fn 𝐴) |
128 | | fndmdif 6992 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴 ∧ 𝑓 Fn 𝐴) → dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓) = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) |
129 | 124, 127,
128 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓) = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) |
130 | 119, 129 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑘} = dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
131 | 130 | unieqd 4879 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ∪
{𝑘} = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
132 | 89, 131 | eqtr3id 2790 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑘 = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
133 | | difeq1 4075 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → (𝑔 ∖ 𝑓) = ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
134 | 133 | dmeqd 5861 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → dom (𝑔 ∖ 𝑓) = dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
135 | 134 | unieqd 4879 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → ∪ dom
(𝑔 ∖ 𝑓) = ∪
dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) |
136 | 135 | rspceeqv 3595 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋 ∧ 𝑘 = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) |
137 | 88, 132, 136 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) |
138 | 137 | ex 413 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) |
139 | 138 | exlimdv 1936 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) |
140 | 65, 139 | syld 47 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) |
141 | 140 | expimpd 454 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ((𝑘 ∈ 𝐴 ∧ ¬ ∪
(𝐹‘𝑘) ≈ 1o) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) |
142 | 17 | breq1d 5115 |
. . . . . . . . 9
⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o)) |
143 | 142 | notbid 317 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (¬ ∪
(𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o)) |
144 | 143 | elrab 3645 |
. . . . . . 7
⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ↔ (𝑘 ∈ 𝐴 ∧ ¬ ∪
(𝐹‘𝑘) ≈ 1o)) |
145 | 39 | elrnmpt 5911 |
. . . . . . . 8
⊢ (𝑘 ∈ V → (𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ↔ ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) |
146 | 145 | elv 3451 |
. . . . . . 7
⊢ (𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ↔ ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) |
147 | 141, 144,
146 | 3imtr4g 295 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)))) |
148 | 147 | ssrdv 3950 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) |
149 | | ssnum 9975 |
. . . . 5
⊢ ((ran
(𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom card ∧ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ dom
card) |
150 | 45, 148, 149 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ dom
card) |
151 | | xpnum 9887 |
. . . 4
⊢ ((X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ dom card)
→ (X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ dom
card) |
152 | 31, 150, 151 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ dom
card) |
153 | 82 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
154 | | rabexg 5288 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
V) |
155 | 153, 154 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
V) |
156 | | fvex 6855 |
. . . . . . 7
⊢ (𝐹‘𝑘) ∈ V |
157 | 156 | uniex 7678 |
. . . . . 6
⊢ ∪ (𝐹‘𝑘) ∈ V |
158 | 157 | rgenw 3068 |
. . . . 5
⊢
∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V |
159 | | iunexg 7896 |
. . . . 5
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) |
160 | 155, 158,
159 | sylancl 586 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) |
161 | | resixp 8871 |
. . . . . 6
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) → (𝑓 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
162 | 24, 49, 161 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑓 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) |
163 | 162 | ne0d 4295 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≠ ∅) |
164 | | ixpiunwdom 9526 |
. . . 4
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ V ∧
∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V ∧ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≠ ∅) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≼* (X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) |
165 | 155, 160,
163, 164 | syl3anc 1371 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≼* (X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) |
166 | | numwdom 9995 |
. . 3
⊢ (((X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ dom card
∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≼* (X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |
167 | 152, 165,
166 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |
168 | 14, 167 | exlimddv 1938 |
1
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |