| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ptcmplem2.7 | . . . 4
⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) | 
| 2 |  | 0ss 4400 | . . . . . . 7
⊢ ∅
⊆ 𝑈 | 
| 3 |  | 0fi 9082 | . . . . . . 7
⊢ ∅
∈ Fin | 
| 4 |  | elfpw 9394 | . . . . . . 7
⊢ (∅
∈ (𝒫 𝑈 ∩
Fin) ↔ (∅ ⊆ 𝑈 ∧ ∅ ∈ Fin)) | 
| 5 | 2, 3, 4 | mpbir2an 711 | . . . . . 6
⊢ ∅
∈ (𝒫 𝑈 ∩
Fin) | 
| 6 |  | unieq 4918 | . . . . . . . 8
⊢ (𝑧 = ∅ → ∪ 𝑧 =
∪ ∅) | 
| 7 |  | uni0 4935 | . . . . . . . 8
⊢ ∪ ∅ = ∅ | 
| 8 | 6, 7 | eqtrdi 2793 | . . . . . . 7
⊢ (𝑧 = ∅ → ∪ 𝑧 =
∅) | 
| 9 | 8 | rspceeqv 3645 | . . . . . 6
⊢ ((∅
∈ (𝒫 𝑈 ∩
Fin) ∧ 𝑋 = ∅)
→ ∃𝑧 ∈
(𝒫 𝑈 ∩
Fin)𝑋 = ∪ 𝑧) | 
| 10 | 5, 9 | mpan 690 | . . . . 5
⊢ (𝑋 = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧) | 
| 11 | 10 | necon3bi 2967 | . . . 4
⊢ (¬
∃𝑧 ∈ (𝒫
𝑈 ∩ Fin)𝑋 = ∪
𝑧 → 𝑋 ≠ ∅) | 
| 12 | 1, 11 | syl 17 | . . 3
⊢ (𝜑 → 𝑋 ≠ ∅) | 
| 13 |  | n0 4353 | . . 3
⊢ (𝑋 ≠ ∅ ↔
∃𝑓 𝑓 ∈ 𝑋) | 
| 14 | 12, 13 | sylib 218 | . 2
⊢ (𝜑 → ∃𝑓 𝑓 ∈ 𝑋) | 
| 15 |  | ptcmp.2 | . . . . . . 7
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) | 
| 16 |  | fveq2 6906 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘)) | 
| 17 | 16 | unieqd 4920 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘)) | 
| 18 | 17 | cbvixpv 8955 | . . . . . . 7
⊢ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) | 
| 19 | 15, 18 | eqtri 2765 | . . . . . 6
⊢ 𝑋 = X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) | 
| 20 |  | ptcmp.5 | . . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) | 
| 21 | 20 | elin2d 4205 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ dom card) | 
| 22 | 21 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ∈ dom card) | 
| 23 | 19, 22 | eqeltrrid 2846 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ∈ dom card) | 
| 24 |  | ssrab2 4080 | . . . . . 6
⊢ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 | 
| 25 | 12 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑋 ≠ ∅) | 
| 26 | 19, 25 | eqnetrrid 3016 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ≠ ∅) | 
| 27 |  | eqid 2737 | . . . . . . 7
⊢ (𝑔 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) = (𝑔 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) | 
| 28 | 27 | resixpfo 8976 | . . . . . 6
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 ∧ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ≠ ∅) → (𝑔 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})):X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘)–onto→X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) | 
| 29 | 24, 26, 28 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘) ↦ (𝑔 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})):X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘)–onto→X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) | 
| 30 |  | fonum 10098 | . . . . 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 3484 | . . . . . . . . . . 11
⊢ 𝑔 ∈ V | 
| 33 |  | difexg 5329 | . . . . . . . . . . 11
⊢ (𝑔 ∈ V → (𝑔 ∖ 𝑓) ∈ V) | 
| 34 | 32, 33 | mp1i 13 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∖ 𝑓) ∈ V) | 
| 35 |  | dmexg 7923 | . . . . . . . . . 10
⊢ ((𝑔 ∖ 𝑓) ∈ V → dom (𝑔 ∖ 𝑓) ∈ V) | 
| 36 |  | uniexg 7760 | . . . . . . . . . 10
⊢ (dom
(𝑔 ∖ 𝑓) ∈ V → ∪ dom (𝑔 ∖ 𝑓) ∈ V) | 
| 37 | 34, 35, 36 | 3syl 18 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪ dom
(𝑔 ∖ 𝑓) ∈ V) | 
| 38 | 37 | ralrimivw 3150 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑔 ∈ 𝑋 ∪ dom (𝑔 ∖ 𝑓) ∈ V) | 
| 39 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) = (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) | 
| 40 | 39 | fnmpt 6708 | . . . . . . . 8
⊢
(∀𝑔 ∈
𝑋 ∪ dom (𝑔 ∖ 𝑓) ∈ V → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋) | 
| 41 | 38, 40 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋) | 
| 42 |  | dffn4 6826 | . . . . . . 7
⊢ ((𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) Fn 𝑋 ↔ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) | 
| 43 | 41, 42 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) | 
| 44 |  | fonum 10098 | . . . . . 6
⊢ ((𝑋 ∈ dom card ∧ (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)):𝑋–onto→ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) → ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom
card) | 
| 45 | 22, 43, 44 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom
card) | 
| 46 |  | ssdif0 4366 | . . . . . . . . . . . 12
⊢ (∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)} ↔ (∪
(𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅) | 
| 47 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) | 
| 48 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋) | 
| 49 | 48, 19 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) | 
| 50 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑓 ∈ V | 
| 51 | 50 | elixp 8944 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))) | 
| 52 | 51 | simprbi 496 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ∪ (𝐹‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) | 
| 53 | 49, 52 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) | 
| 54 | 53 | r19.21bi 3251 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)) | 
| 55 | 54 | snssd 4809 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → {(𝑓‘𝑘)} ⊆ ∪
(𝐹‘𝑘)) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → {(𝑓‘𝑘)} ⊆ ∪
(𝐹‘𝑘)) | 
| 57 | 47, 56 | eqssd 4001 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) = {(𝑓‘𝑘)}) | 
| 58 |  | fvex 6919 | . . . . . . . . . . . . . . 15
⊢ (𝑓‘𝑘) ∈ V | 
| 59 | 58 | ensn1 9061 | . . . . . . . . . . . . . 14
⊢ {(𝑓‘𝑘)} ≈ 1o | 
| 60 | 57, 59 | eqbrtrdi 5182 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ {(𝑓‘𝑘)}) → ∪
(𝐹‘𝑘) ≈ 1o) | 
| 61 | 60 | ex 412 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (∪
(𝐹‘𝑘) ⊆ {(𝑓‘𝑘)} → ∪ (𝐹‘𝑘) ≈ 1o)) | 
| 62 | 46, 61 | biimtrrid 243 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → ((∪
(𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅ → ∪ (𝐹‘𝑘) ≈ 1o)) | 
| 63 | 62 | con3d 152 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ¬ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅)) | 
| 64 |  | neq0 4352 | . . . . . . . . . 10
⊢ (¬
(∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) = ∅ ↔ ∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) | 
| 65 | 63, 64 | imbitrdi 251 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}))) | 
| 66 |  | eldifi 4131 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → 𝑥 ∈ ∪ (𝐹‘𝑘)) | 
| 67 |  | simplr 769 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → 𝑥 ∈ ∪ (𝐹‘𝑘)) | 
| 68 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = 𝑥) | 
| 69 | 68, 17 | eleq12d 2835 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛) ↔ 𝑥 ∈ ∪ (𝐹‘𝑘))) | 
| 70 | 67, 69 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) | 
| 71 | 48, 15 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) | 
| 72 | 50 | elixp 8944 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) | 
| 73 | 72 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) | 
| 74 | 71, 73 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) | 
| 75 | 74 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) | 
| 76 | 75 | r19.21bi 3251 | . . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)) | 
| 77 |  | iffalse 4534 | . . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = (𝑓‘𝑛)) | 
| 78 | 77 | eleq1d 2826 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑛 = 𝑘 → (if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))) | 
| 79 | 76, 78 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → (¬ 𝑛 = 𝑘 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) | 
| 80 | 70, 79 | pm2.61d 179 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) ∧ 𝑛 ∈ 𝐴) → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛)) | 
| 81 | 80 | ralrimiva 3146 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛)) | 
| 82 |  | ptcmp.3 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 83 | 82 | ad3antrrr 730 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → 𝐴 ∈ 𝑉) | 
| 84 |  | mptelixpg 8975 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 𝑉 → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ ∀𝑛 ∈ 𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ ∪ (𝐹‘𝑛))) | 
| 86 | 81, 85 | mpbird 257 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)) | 
| 87 | 86, 15 | eleqtrrdi 2852 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ ∪ (𝐹‘𝑘)) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋) | 
| 88 | 66, 87 | sylan2 593 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋) | 
| 89 |  | unisnv 4927 | . . . . . . . . . . . . 13
⊢ ∪ {𝑘}
= 𝑘 | 
| 90 |  | simplr 769 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑘 ∈ 𝐴) | 
| 91 |  | eleq1w 2824 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑘 → (𝑚 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴)) | 
| 92 | 90, 91 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 → 𝑚 ∈ 𝐴)) | 
| 93 | 92 | pm4.71rd 562 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘))) | 
| 94 |  | equequ1 2024 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑛 = 𝑘 ↔ 𝑚 = 𝑘)) | 
| 95 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚)) | 
| 96 | 94, 95 | ifbieq2d 4552 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) = if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚))) | 
| 97 |  | eqid 2737 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) | 
| 98 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑥 ∈ V | 
| 99 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓‘𝑚) ∈ V | 
| 100 | 98, 99 | ifex 4576 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ∈ V | 
| 101 | 96, 97, 100 | fvmpt 7016 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ 𝐴 → ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) = if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚))) | 
| 102 | 101 | neeq1d 3000 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ 𝐴 → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) | 
| 103 | 102 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) | 
| 104 |  | iffalse 4534 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) = (𝑓‘𝑚)) | 
| 105 | 104 | necon1ai 2968 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) → 𝑚 = 𝑘) | 
| 106 |  | eldifsni 4790 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → 𝑥 ≠ (𝑓‘𝑘)) | 
| 107 | 106 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → 𝑥 ≠ (𝑓‘𝑘)) | 
| 108 |  | iftrue 4531 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) = 𝑥) | 
| 109 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑘 → (𝑓‘𝑚) = (𝑓‘𝑘)) | 
| 110 | 108, 109 | neeq12d 3002 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑘 → (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) ↔ 𝑥 ≠ (𝑓‘𝑘))) | 
| 111 | 107, 110 | syl5ibrcom 247 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (𝑚 = 𝑘 → if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚))) | 
| 112 | 105, 111 | impbid2 226 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (if(𝑚 = 𝑘, 𝑥, (𝑓‘𝑚)) ≠ (𝑓‘𝑚) ↔ 𝑚 = 𝑘)) | 
| 113 | 103, 112 | bitrd 279 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) ∧ 𝑚 ∈ 𝐴) → (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚) ↔ 𝑚 = 𝑘)) | 
| 114 | 113 | pm5.32da 579 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ((𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)) ↔ (𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘))) | 
| 115 | 93, 114 | bitr4d 282 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑚 = 𝑘 ↔ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)))) | 
| 116 | 115 | abbidv 2808 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑚 ∣ 𝑚 = 𝑘} = {𝑚 ∣ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚))}) | 
| 117 |  | df-sn 4627 | . . . . . . . . . . . . . . . 16
⊢ {𝑘} = {𝑚 ∣ 𝑚 = 𝑘} | 
| 118 |  | df-rab 3437 | . . . . . . . . . . . . . . . 16
⊢ {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)} = {𝑚 ∣ (𝑚 ∈ 𝐴 ∧ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚))} | 
| 119 | 116, 117,
118 | 3eqtr4g 2802 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑘} = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) | 
| 120 |  | fvex 6919 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓‘𝑛) ∈ V | 
| 121 | 98, 120 | ifex 4576 | . . . . . . . . . . . . . . . . . 18
⊢ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V | 
| 122 | 121 | rgenw 3065 | . . . . . . . . . . . . . . . . 17
⊢
∀𝑛 ∈
𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V | 
| 123 | 97 | fnmpt 6708 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑛 ∈
𝐴 if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)) ∈ V → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴) | 
| 124 | 122, 123 | mp1i 13 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴) | 
| 125 |  | ixpfn 8943 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) → 𝑓 Fn 𝐴) | 
| 126 | 71, 125 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝑓 Fn 𝐴) | 
| 127 | 126 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑓 Fn 𝐴) | 
| 128 |  | fndmdif 7062 | . . . . . . . . . . . . . . . 16
⊢ (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) Fn 𝐴 ∧ 𝑓 Fn 𝐴) → dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓) = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) | 
| 129 | 124, 127,
128 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓) = {𝑚 ∈ 𝐴 ∣ ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛)))‘𝑚) ≠ (𝑓‘𝑚)}) | 
| 130 | 119, 129 | eqtr4d 2780 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → {𝑘} = dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 131 | 130 | unieqd 4920 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ∪
{𝑘} = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 132 | 89, 131 | eqtr3id 2791 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → 𝑘 = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 133 |  | difeq1 4119 | . . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → (𝑔 ∖ 𝑓) = ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 134 | 133 | dmeqd 5916 | . . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → dom (𝑔 ∖ 𝑓) = dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 135 | 134 | unieqd 4920 | . . . . . . . . . . . . 13
⊢ (𝑔 = (𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) → ∪ dom
(𝑔 ∖ 𝑓) = ∪
dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) | 
| 136 | 135 | rspceeqv 3645 | . . . . . . . . . . . 12
⊢ (((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∈ 𝑋 ∧ 𝑘 = ∪ dom ((𝑛 ∈ 𝐴 ↦ if(𝑛 = 𝑘, 𝑥, (𝑓‘𝑛))) ∖ 𝑓)) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) | 
| 137 | 88, 132, 136 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) ∧ 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)})) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) | 
| 138 | 137 | ex 412 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) | 
| 139 | 138 | exlimdv 1933 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (∃𝑥 𝑥 ∈ (∪ (𝐹‘𝑘) ∖ {(𝑓‘𝑘)}) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) | 
| 140 | 65, 139 | syld 47 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝑋) ∧ 𝑘 ∈ 𝐴) → (¬ ∪
(𝐹‘𝑘) ≈ 1o → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) | 
| 141 | 140 | expimpd 453 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ((𝑘 ∈ 𝐴 ∧ ¬ ∪
(𝐹‘𝑘) ≈ 1o) → ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) | 
| 142 | 17 | breq1d 5153 | . . . . . . . . 9
⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o)) | 
| 143 | 142 | notbid 318 | . . . . . . . 8
⊢ (𝑛 = 𝑘 → (¬ ∪
(𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o)) | 
| 144 | 143 | elrab 3692 | . . . . . . 7
⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ↔ (𝑘 ∈ 𝐴 ∧ ¬ ∪
(𝐹‘𝑘) ≈ 1o)) | 
| 145 | 39 | elrnmpt 5969 | . . . . . . . 8
⊢ (𝑘 ∈ V → (𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ↔ ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓))) | 
| 146 | 145 | elv 3485 | . . . . . . 7
⊢ (𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ↔ ∃𝑔 ∈ 𝑋 𝑘 = ∪ dom (𝑔 ∖ 𝑓)) | 
| 147 | 141, 144,
146 | 3imtr4g 296 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)))) | 
| 148 | 147 | ssrdv 3989 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) | 
| 149 |  | ssnum 10079 | . . . . 5
⊢ ((ran
(𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓)) ∈ dom card ∧ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ ran (𝑔 ∈ 𝑋 ↦ ∪ dom
(𝑔 ∖ 𝑓))) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ dom
card) | 
| 150 | 45, 148, 149 | syl2anc 584 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ dom
card) | 
| 151 |  | xpnum 9991 | . . . 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 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → 𝐴 ∈ 𝑉) | 
| 154 |  | rabexg 5337 | . . . . 5
⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
V) | 
| 155 | 153, 154 | syl 17 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈
V) | 
| 156 |  | fvex 6919 | . . . . . . 7
⊢ (𝐹‘𝑘) ∈ V | 
| 157 | 156 | uniex 7761 | . . . . . 6
⊢ ∪ (𝐹‘𝑘) ∈ V | 
| 158 | 157 | rgenw 3065 | . . . . 5
⊢
∀𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V | 
| 159 |  | iunexg 7988 | . . . . 5
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ V ∧
∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) | 
| 160 | 155, 158,
159 | sylancl 586 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V) | 
| 161 |  | resixp 8973 | . . . . . 6
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ⊆ 𝐴 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ∪ (𝐹‘𝑘)) → (𝑓 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) | 
| 162 | 24, 49, 161 | sylancr 587 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → (𝑓 ↾ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}) ∈ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) | 
| 163 | 162 | ne0d 4342 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → X𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≠ ∅) | 
| 164 |  | ixpiunwdom 9630 | . . . 4
⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o} ∈ V ∧
∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ V ∧ X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≠ ∅) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≼* (X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) | 
| 165 | 155, 160,
163, 164 | syl3anc 1373 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑋) → ∪
𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ≼* (X𝑘 ∈
{𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) × {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o})) | 
| 166 |  | numwdom 10099 | . . 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 1935 | 1
⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪
(𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card) |