| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvex 6918 | . . . 4
⊢
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ V | 
| 2 | 1 | sucid 6465 | . . 3
⊢
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) | 
| 3 |  | ttukeylem.1 | . . . 4
⊢ (𝜑 → 𝐹:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 4 |  | ttukeylem.2 | . . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐴) | 
| 5 |  | ttukeylem.3 | . . . 4
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) | 
| 6 |  | ttukeylem.4 | . . . 4
⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))) | 
| 7 | 3, 4, 5, 6 | ttukeylem6 10555 | . . 3
⊢ ((𝜑 ∧ (card‘(∪ 𝐴
∖ 𝐵)) ∈ suc
(card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ∈ 𝐴) | 
| 8 | 2, 7 | mpan2 691 | . 2
⊢ (𝜑 → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ∈ 𝐴) | 
| 9 | 3, 4, 5, 6 | ttukeylem4 10553 | . . 3
⊢ (𝜑 → (𝐺‘∅) = 𝐵) | 
| 10 |  | 0elon 6437 | . . . . 5
⊢ ∅
∈ On | 
| 11 |  | cardon 9985 | . . . . 5
⊢
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On | 
| 12 |  | 0ss 4399 | . . . . 5
⊢ ∅
⊆ (card‘(∪ 𝐴 ∖ 𝐵)) | 
| 13 | 10, 11, 12 | 3pm3.2i 1339 | . . . 4
⊢ (∅
∈ On ∧ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ ∅ ⊆
(card‘(∪ 𝐴 ∖ 𝐵))) | 
| 14 | 3, 4, 5, 6 | ttukeylem5 10554 | . . . 4
⊢ ((𝜑 ∧ (∅ ∈ On ∧
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ ∅ ⊆
(card‘(∪ 𝐴 ∖ 𝐵)))) → (𝐺‘∅) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 15 | 13, 14 | mpan2 691 | . . 3
⊢ (𝜑 → (𝐺‘∅) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 16 | 9, 15 | eqsstrrd 4018 | . 2
⊢ (𝜑 → 𝐵 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 17 |  | simprr 772 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) | 
| 18 |  | ssun1 4177 | . . . . . . . 8
⊢ 𝑦 ⊆ (𝑦 ∪ 𝐵) | 
| 19 |  | undif1 4475 | . . . . . . . 8
⊢ ((𝑦 ∖ 𝐵) ∪ 𝐵) = (𝑦 ∪ 𝐵) | 
| 20 | 18, 19 | sseqtrri 4032 | . . . . . . 7
⊢ 𝑦 ⊆ ((𝑦 ∖ 𝐵) ∪ 𝐵) | 
| 21 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝜑) | 
| 22 |  | f1ocnv 6859 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) → ◡𝐹:(∪ 𝐴 ∖ 𝐵)–1-1-onto→(card‘(∪
𝐴 ∖ 𝐵))) | 
| 23 |  | f1of 6847 | . . . . . . . . . . . . . . . . 17
⊢ (◡𝐹:(∪ 𝐴 ∖ 𝐵)–1-1-onto→(card‘(∪
𝐴 ∖ 𝐵)) → ◡𝐹:(∪ 𝐴 ∖ 𝐵)⟶(card‘(∪ 𝐴
∖ 𝐵))) | 
| 24 | 3, 22, 23 | 3syl 18 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ◡𝐹:(∪ 𝐴 ∖ 𝐵)⟶(card‘(∪ 𝐴
∖ 𝐵))) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ◡𝐹:(∪ 𝐴 ∖ 𝐵)⟶(card‘(∪ 𝐴
∖ 𝐵))) | 
| 26 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (𝑦 ∖ 𝐵) → 𝑎 ∈ 𝑦) | 
| 27 | 26 | ad2antll 729 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ 𝑦) | 
| 28 |  | simprll 778 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑦 ∈ 𝐴) | 
| 29 |  | elunii 4911 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑎 ∈ ∪ 𝐴) | 
| 30 | 27, 28, 29 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ ∪ 𝐴) | 
| 31 |  | eldifn 4131 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (𝑦 ∖ 𝐵) → ¬ 𝑎 ∈ 𝐵) | 
| 32 | 31 | ad2antll 729 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ¬ 𝑎 ∈ 𝐵) | 
| 33 | 30, 32 | eldifd 3961 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ (∪ 𝐴 ∖ 𝐵)) | 
| 34 | 25, 33 | ffvelcdmd 7104 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (◡𝐹‘𝑎) ∈ (card‘(∪ 𝐴
∖ 𝐵))) | 
| 35 |  | onelon 6408 | . . . . . . . . . . . . . 14
⊢
(((card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ (◡𝐹‘𝑎) ∈ (card‘(∪ 𝐴
∖ 𝐵))) → (◡𝐹‘𝑎) ∈ On) | 
| 36 | 11, 34, 35 | sylancr 587 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (◡𝐹‘𝑎) ∈ On) | 
| 37 |  | onsuc 7832 | . . . . . . . . . . . . 13
⊢ ((◡𝐹‘𝑎) ∈ On → suc (◡𝐹‘𝑎) ∈ On) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → suc (◡𝐹‘𝑎) ∈ On) | 
| 39 | 11 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (card‘(∪ 𝐴
∖ 𝐵)) ∈
On) | 
| 40 | 11 | onordi 6494 | . . . . . . . . . . . . 13
⊢ Ord
(card‘(∪ 𝐴 ∖ 𝐵)) | 
| 41 |  | ordsucss 7839 | . . . . . . . . . . . . 13
⊢ (Ord
(card‘(∪ 𝐴 ∖ 𝐵)) → ((◡𝐹‘𝑎) ∈ (card‘(∪ 𝐴
∖ 𝐵)) → suc
(◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵)))) | 
| 42 | 40, 34, 41 | mpsyl 68 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → suc (◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵))) | 
| 43 | 3, 4, 5, 6 | ttukeylem5 10554 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (suc (◡𝐹‘𝑎) ∈ On ∧ (card‘(∪ 𝐴
∖ 𝐵)) ∈ On ∧
suc (◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵)))) → (𝐺‘suc (◡𝐹‘𝑎)) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 44 | 21, 38, 39, 42, 43 | syl13anc 1373 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘suc (◡𝐹‘𝑎)) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 45 |  | ssun2 4178 | . . . . . . . . . . . . 13
⊢
if(((𝐺‘∪ suc (◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅) ⊆ ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅)) | 
| 46 |  | eloni 6393 | . . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹‘𝑎) ∈ On → Ord (◡𝐹‘𝑎)) | 
| 47 |  | ordunisuc 7853 | . . . . . . . . . . . . . . . . . 18
⊢ (Ord
(◡𝐹‘𝑎) → ∪ suc
(◡𝐹‘𝑎) = (◡𝐹‘𝑎)) | 
| 48 | 36, 46, 47 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ∪ suc
(◡𝐹‘𝑎) = (◡𝐹‘𝑎)) | 
| 49 | 48 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐹‘∪ suc
(◡𝐹‘𝑎)) = (𝐹‘(◡𝐹‘𝑎))) | 
| 50 | 3 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝐹:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 51 |  | f1ocnvfv2 7298 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐹:(card‘(∪ 𝐴
∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵) ∧ 𝑎 ∈ (∪ 𝐴 ∖ 𝐵)) → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) | 
| 52 | 50, 33, 51 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐹‘(◡𝐹‘𝑎)) = 𝑎) | 
| 53 | 49, 52 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 = (𝐹‘∪ suc
(◡𝐹‘𝑎))) | 
| 54 |  | velsn 4641 | . . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ {(𝐹‘∪ suc
(◡𝐹‘𝑎))} ↔ 𝑎 = (𝐹‘∪ suc
(◡𝐹‘𝑎))) | 
| 55 | 53, 54 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) | 
| 56 | 48 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘∪ suc
(◡𝐹‘𝑎)) = (𝐺‘(◡𝐹‘𝑎))) | 
| 57 |  | ordelss 6399 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord
(card‘(∪ 𝐴 ∖ 𝐵)) ∧ (◡𝐹‘𝑎) ∈ (card‘(∪ 𝐴
∖ 𝐵))) → (◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵))) | 
| 58 | 40, 34, 57 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵))) | 
| 59 | 3, 4, 5, 6 | ttukeylem5 10554 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ ((◡𝐹‘𝑎) ∈ On ∧ (card‘(∪ 𝐴
∖ 𝐵)) ∈ On ∧
(◡𝐹‘𝑎) ⊆ (card‘(∪ 𝐴
∖ 𝐵)))) → (𝐺‘(◡𝐹‘𝑎)) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 60 | 21, 36, 39, 58, 59 | syl13anc 1373 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘(◡𝐹‘𝑎)) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 61 | 56, 60 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘∪ suc
(◡𝐹‘𝑎)) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 62 |  | simprlr 779 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) | 
| 63 | 61, 62 | sstrd 3993 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘∪ suc
(◡𝐹‘𝑎)) ⊆ 𝑦) | 
| 64 | 53, 27 | eqeltrrd 2841 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐹‘∪ suc
(◡𝐹‘𝑎)) ∈ 𝑦) | 
| 65 | 64 | snssd 4808 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → {(𝐹‘∪ suc
(◡𝐹‘𝑎))} ⊆ 𝑦) | 
| 66 | 63, 65 | unssd 4191 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ⊆ 𝑦) | 
| 67 | 3, 4, 5 | ttukeylem2 10551 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ⊆ 𝑦)) → ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴) | 
| 68 | 21, 28, 66, 67 | syl12anc 836 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴) | 
| 69 | 68 | iftrued 4532 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅) = {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) | 
| 70 | 55, 69 | eleqtrrd 2843 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅)) | 
| 71 | 45, 70 | sselid 3980 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅))) | 
| 72 | 3, 4, 5, 6 | ttukeylem3 10552 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ suc (◡𝐹‘𝑎) ∈ On) → (𝐺‘suc (◡𝐹‘𝑎)) = if(suc (◡𝐹‘𝑎) = ∪ suc (◡𝐹‘𝑎), if(suc (◡𝐹‘𝑎) = ∅, 𝐵, ∪ (𝐺 “ suc (◡𝐹‘𝑎))), ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅)))) | 
| 73 | 38, 72 | syldan 591 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘suc (◡𝐹‘𝑎)) = if(suc (◡𝐹‘𝑎) = ∪ suc (◡𝐹‘𝑎), if(suc (◡𝐹‘𝑎) = ∅, 𝐵, ∪ (𝐺 “ suc (◡𝐹‘𝑎))), ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅)))) | 
| 74 |  | sucidg 6464 | . . . . . . . . . . . . . . . . . 18
⊢ ((◡𝐹‘𝑎) ∈ (card‘(∪ 𝐴
∖ 𝐵)) → (◡𝐹‘𝑎) ∈ suc (◡𝐹‘𝑎)) | 
| 75 | 34, 74 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (◡𝐹‘𝑎) ∈ suc (◡𝐹‘𝑎)) | 
| 76 |  | ordirr 6401 | . . . . . . . . . . . . . . . . . 18
⊢ (Ord
(◡𝐹‘𝑎) → ¬ (◡𝐹‘𝑎) ∈ (◡𝐹‘𝑎)) | 
| 77 | 36, 46, 76 | 3syl 18 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ¬ (◡𝐹‘𝑎) ∈ (◡𝐹‘𝑎)) | 
| 78 |  | nelne1 3038 | . . . . . . . . . . . . . . . . 17
⊢ (((◡𝐹‘𝑎) ∈ suc (◡𝐹‘𝑎) ∧ ¬ (◡𝐹‘𝑎) ∈ (◡𝐹‘𝑎)) → suc (◡𝐹‘𝑎) ≠ (◡𝐹‘𝑎)) | 
| 79 | 75, 77, 78 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → suc (◡𝐹‘𝑎) ≠ (◡𝐹‘𝑎)) | 
| 80 | 79, 48 | neeqtrrd 3014 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → suc (◡𝐹‘𝑎) ≠ ∪ suc
(◡𝐹‘𝑎)) | 
| 81 | 80 | neneqd 2944 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → ¬ suc (◡𝐹‘𝑎) = ∪ suc (◡𝐹‘𝑎)) | 
| 82 | 81 | iffalsed 4535 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → if(suc (◡𝐹‘𝑎) = ∪ suc (◡𝐹‘𝑎), if(suc (◡𝐹‘𝑎) = ∅, 𝐵, ∪ (𝐺 “ suc (◡𝐹‘𝑎))), ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅))) = ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅))) | 
| 83 | 73, 82 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → (𝐺‘suc (◡𝐹‘𝑎)) = ((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ if(((𝐺‘∪ suc
(◡𝐹‘𝑎)) ∪ {(𝐹‘∪ suc
(◡𝐹‘𝑎))}) ∈ 𝐴, {(𝐹‘∪ suc
(◡𝐹‘𝑎))}, ∅))) | 
| 84 | 71, 83 | eleqtrrd 2843 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ (𝐺‘suc (◡𝐹‘𝑎))) | 
| 85 | 44, 84 | sseldd 3983 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦) ∧ 𝑎 ∈ (𝑦 ∖ 𝐵))) → 𝑎 ∈ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 86 | 85 | expr 456 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → (𝑎 ∈ (𝑦 ∖ 𝐵) → 𝑎 ∈ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))))) | 
| 87 | 86 | ssrdv 3988 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → (𝑦 ∖ 𝐵) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 88 | 16 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → 𝐵 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 89 | 87, 88 | unssd 4191 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → ((𝑦 ∖ 𝐵) ∪ 𝐵) ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 90 | 20, 89 | sstrid 3994 | . . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → 𝑦 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵)))) | 
| 91 | 17, 90 | eqssd 4000 | . . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦)) → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) = 𝑦) | 
| 92 | 91 | expr 456 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ((𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦 → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) = 𝑦)) | 
| 93 |  | npss 4112 | . . . 4
⊢ (¬
(𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦 ↔ ((𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊆ 𝑦 → (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) = 𝑦)) | 
| 94 | 92, 93 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦) | 
| 95 | 94 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦) | 
| 96 |  | sseq2 4009 | . . . 4
⊢ (𝑥 = (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) → (𝐵 ⊆ 𝑥 ↔ 𝐵 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))))) | 
| 97 |  | psseq1 4089 | . . . . . 6
⊢ (𝑥 = (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) → (𝑥 ⊊ 𝑦 ↔ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦)) | 
| 98 | 97 | notbid 318 | . . . . 5
⊢ (𝑥 = (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) → (¬
𝑥 ⊊ 𝑦 ↔ ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦)) | 
| 99 | 98 | ralbidv 3177 | . . . 4
⊢ (𝑥 = (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦)) | 
| 100 | 96, 99 | anbi12d 632 | . . 3
⊢ (𝑥 = (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) → ((𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) ↔ (𝐵 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ∧
∀𝑦 ∈ 𝐴 ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦))) | 
| 101 | 100 | rspcev 3621 | . 2
⊢ (((𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ∈ 𝐴 ∧ (𝐵 ⊆ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ∧
∀𝑦 ∈ 𝐴 ¬ (𝐺‘(card‘(∪ 𝐴
∖ 𝐵))) ⊊ 𝑦)) → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) | 
| 102 | 8, 16, 95, 101 | syl12anc 836 | 1
⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑥 ∧ ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |