| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | difss 4136 | . . . 4
⊢ (∪ 𝐴
∖ 𝐵) ⊆ ∪ 𝐴 | 
| 2 |  | ssnum 10079 | . . . 4
⊢ ((∪ 𝐴
∈ dom card ∧ (∪ 𝐴 ∖ 𝐵) ⊆ ∪ 𝐴) → (∪ 𝐴
∖ 𝐵) ∈ dom
card) | 
| 3 | 1, 2 | mpan2 691 | . . 3
⊢ (∪ 𝐴
∈ dom card → (∪ 𝐴 ∖ 𝐵) ∈ dom card) | 
| 4 |  | isnum3 9994 | . . . . 5
⊢ ((∪ 𝐴
∖ 𝐵) ∈ dom card
↔ (card‘(∪ 𝐴 ∖ 𝐵)) ≈ (∪
𝐴 ∖ 𝐵)) | 
| 5 |  | bren 8995 | . . . . 5
⊢
((card‘(∪ 𝐴 ∖ 𝐵)) ≈ (∪
𝐴 ∖ 𝐵) ↔ ∃𝑓 𝑓:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 6 | 4, 5 | bitri 275 | . . . 4
⊢ ((∪ 𝐴
∖ 𝐵) ∈ dom card
↔ ∃𝑓 𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 7 |  | simp1 1137 | . . . . . . 7
⊢ ((𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) ∧ 𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → 𝑓:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 8 |  | simp2 1138 | . . . . . . 7
⊢ ((𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) ∧ 𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → 𝐵 ∈ 𝐴) | 
| 9 |  | simp3 1139 | . . . . . . 7
⊢ ((𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) ∧ 𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) | 
| 10 |  | dmeq 5914 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → dom 𝑤 = dom 𝑧) | 
| 11 | 10 | unieqd 4920 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → ∪ dom
𝑤 = ∪ dom 𝑧) | 
| 12 | 10, 11 | eqeq12d 2753 | . . . . . . . . . 10
⊢ (𝑤 = 𝑧 → (dom 𝑤 = ∪ dom 𝑤 ↔ dom 𝑧 = ∪ dom 𝑧)) | 
| 13 | 10 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (dom 𝑤 = ∅ ↔ dom 𝑧 = ∅)) | 
| 14 |  | rneq 5947 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → ran 𝑤 = ran 𝑧) | 
| 15 | 14 | unieqd 4920 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → ∪ ran
𝑤 = ∪ ran 𝑧) | 
| 16 | 13, 15 | ifbieq2d 4552 | . . . . . . . . . 10
⊢ (𝑤 = 𝑧 → if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤) = if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧)) | 
| 17 |  | id 22 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) | 
| 18 | 17, 11 | fveq12d 6913 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → (𝑤‘∪ dom 𝑤) = (𝑧‘∪ dom 𝑧)) | 
| 19 | 11 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → (𝑓‘∪ dom 𝑤) = (𝑓‘∪ dom 𝑧)) | 
| 20 | 19 | sneqd 4638 | . . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → {(𝑓‘∪ dom 𝑤)} = {(𝑓‘∪ dom 𝑧)}) | 
| 21 | 18, 20 | uneq12d 4169 | . . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → ((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) = ((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)})) | 
| 22 | 21 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴 ↔ ((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴)) | 
| 23 | 22, 20 | ifbieq1d 4550 | . . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅) = if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)}, ∅)) | 
| 24 | 18, 23 | uneq12d 4169 | . . . . . . . . . 10
⊢ (𝑤 = 𝑧 → ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅)) = ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)}, ∅))) | 
| 25 | 12, 16, 24 | ifbieq12d 4554 | . . . . . . . . 9
⊢ (𝑤 = 𝑧 → if(dom 𝑤 = ∪ dom 𝑤, if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤), ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅))) = if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)}, ∅)))) | 
| 26 | 25 | cbvmptv 5255 | . . . . . . . 8
⊢ (𝑤 ∈ V ↦ if(dom 𝑤 = ∪
dom 𝑤, if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤), ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)}, ∅)))) | 
| 27 |  | recseq 8414 | . . . . . . . 8
⊢ ((𝑤 ∈ V ↦ if(dom 𝑤 = ∪
dom 𝑤, if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤), ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)}, ∅)))) →
recs((𝑤 ∈ V ↦
if(dom 𝑤 = ∪ dom 𝑤, if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤), ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅))))) = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)},
∅)))))) | 
| 28 | 26, 27 | ax-mp 5 | . . . . . . 7
⊢
recs((𝑤 ∈ V
↦ if(dom 𝑤 = ∪ dom 𝑤, if(dom 𝑤 = ∅, 𝐵, ∪ ran 𝑤), ((𝑤‘∪ dom 𝑤) ∪ if(((𝑤‘∪ dom 𝑤) ∪ {(𝑓‘∪ dom 𝑤)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑤)}, ∅))))) = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝑓‘∪ dom 𝑧)}) ∈ 𝐴, {(𝑓‘∪ dom 𝑧)},
∅))))) | 
| 29 | 7, 8, 9, 28 | ttukeylem7 10555 | . . . . . 6
⊢ ((𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) ∧ 𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) | 
| 30 | 29 | 3expib 1123 | . . . . 5
⊢ (𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) → ((𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦))) | 
| 31 | 30 | exlimiv 1930 | . . . 4
⊢
(∃𝑓 𝑓:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) → ((𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦))) | 
| 32 | 6, 31 | sylbi 217 | . . 3
⊢ ((∪ 𝐴
∖ 𝐵) ∈ dom card
→ ((𝐵 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦))) | 
| 33 | 3, 32 | syl 17 | . 2
⊢ (∪ 𝐴
∈ dom card → ((𝐵
∈ 𝐴 ∧
∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦))) | 
| 34 | 33 | 3impib 1117 | 1
⊢ ((∪ 𝐴
∈ dom card ∧ 𝐵
∈ 𝐴 ∧
∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |