Step | Hyp | Ref
| Expression |
1 | | cardon 8770 |
. . . . 5
⊢
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On |
2 | 1 | onsuci 7038 |
. . . 4
⊢ suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → suc (card‘(∪ 𝐴
∖ 𝐵)) ∈
On) |
4 | | onelon 5748 |
. . 3
⊢ ((suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝐶 ∈ On) |
5 | 3, 4 | sylan 488 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝐶 ∈ On) |
6 | | eleq1 2689 |
. . . . . 6
⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)))) |
7 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎)) |
8 | 7 | eleq1d 2686 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴)) |
9 | 6, 8 | imbi12d 334 |
. . . . 5
⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
10 | 9 | imbi2d 330 |
. . . 4
⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))) |
11 | | eleq1 2689 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)))) |
12 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶)) |
13 | 12 | eleq1d 2686 |
. . . . . 6
⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴)) |
14 | 11, 13 | imbi12d 334 |
. . . . 5
⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))) |
15 | 14 | imbi2d 330 |
. . . 4
⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))) |
16 | | r19.21v 2960 |
. . . . . 6
⊢
(∀𝑎 ∈
𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
17 | 2 | onordi 5832 |
. . . . . . . . . . . . . . 15
⊢ Ord suc
(card‘(∪ 𝐴 ∖ 𝐵)) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Ord suc (card‘(∪ 𝐴
∖ 𝐵))) |
19 | | ordelss 5739 |
. . . . . . . . . . . . . 14
⊢ ((Ord suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴
∖ 𝐵))) |
20 | 18, 19 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴
∖ 𝐵))) |
21 | 20 | sselda 3603 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → 𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) |
22 | | biimt 350 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
24 | 23 | ralbidva 2985 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
25 | 2 | onssi 7037 |
. . . . . . . . . . . . . 14
⊢ suc
(card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On |
26 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) |
27 | 25, 26 | sseldi 3601 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ On) |
28 | | ttukeylem.1 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) |
29 | | ttukeylem.2 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
30 | | ttukeylem.3 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) |
31 | | ttukeylem.4 |
. . . . . . . . . . . . . 14
⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))) |
32 | 28, 29, 30, 31 | ttukeylem3 9333 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) |
33 | 27, 32 | syldan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) |
34 | 29 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴) |
35 | | inss2 3834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ Fin |
36 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ (𝒫
∪ (𝐺 “ 𝑦) ∩ Fin)) |
37 | 35, 36 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈
Fin) |
38 | | inss1 3833 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝒫 ∪ (𝐺
“ 𝑦) |
39 | 38, 36 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ 𝒫
∪ (𝐺 “ 𝑦)) |
40 | 39 | elpwid 4170 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ⊆ ∪ (𝐺
“ 𝑦)) |
41 | 31 | tfr1 7493 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 Fn On |
42 | | fnfun 5988 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 Fn On → Fun 𝐺) |
43 | | funiunfv 6506 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)) |
44 | 41, 42, 43 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦) |
45 | 40, 44 | syl6sseqr 3652 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣)) |
46 | | dfss3 3592 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪
𝑣 ∈ 𝑦 (𝐺‘𝑣)) |
47 | | eliun 4524 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
48 | 47 | ralbii 2980 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑢 ∈
𝑤 𝑢 ∈ ∪
𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
49 | 46, 48 | bitri 264 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
50 | 45, 49 | sylib 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ∀𝑢 ∈
𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
51 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢))) |
52 | 51 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
53 | 52 | ac6sfi 8204 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
54 | 37, 50, 53 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
55 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
56 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑) |
57 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦) |
58 | 57 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦) |
59 | | frn 6053 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦) |
61 | 27 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On) |
62 | | onss 6990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ On → 𝑦 ⊆ On) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On) |
64 | 60, 63 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On) |
65 | 37 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin) |
67 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤) |
68 | 58, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤) |
69 | | dffn4 6121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓) |
70 | 68, 69 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓) |
71 | | fofi 8252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
72 | 66, 70, 71 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin) |
73 | | dm0rn0 5342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
74 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:𝑤⟶𝑦 → dom 𝑓 = 𝑤) |
75 | 57, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤) |
76 | 75 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅)) |
77 | 73, 76 | syl5bbr 274 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅)) |
78 | 77 | necon3bid 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
79 | 78 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅) |
80 | | ordunifi 8210 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ran
𝑓 ⊆ On ∧ ran
𝑓 ∈ Fin ∧ ran
𝑓 ≠ ∅) →
∪ ran 𝑓 ∈ ran 𝑓) |
81 | 64, 72, 79, 80 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓) |
82 | 60, 81 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦) |
83 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
84 | 83 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
85 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = ∪
ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran
𝑓)) |
86 | 85 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = ∪
ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran
𝑓) ∈ 𝐴)) |
87 | 86 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∪ ran 𝑓 ∈ 𝑦 → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘∪ ran
𝑓) ∈ 𝐴)) |
88 | 82, 84, 87 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran
𝑓) ∈ 𝐴) |
89 | | simp-4l 806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑) |
90 | 27 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On) |
91 | 90, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On) |
92 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦) |
93 | 92 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦) |
94 | 91, 93 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On) |
95 | 59 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦) |
96 | 95, 91 | sstrd 3613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On) |
97 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑓 ∈ V |
98 | 97 | rnex 7100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ran 𝑓 ∈ V |
99 | 98 | ssonunii 6987 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (ran
𝑓 ⊆ On → ∪ ran 𝑓 ∈ On) |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran
𝑓 ∈
On) |
101 | 67 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤) |
102 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤) |
103 | | fnfvelrn 6356 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓) |
104 | 101, 102,
103 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓) |
105 | | elssuni 4467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran
𝑓) |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran
𝑓) |
107 | 28, 29, 30, 31 | ttukeylem5 9335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran
𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran
𝑓)) |
108 | 89, 94, 100, 106, 107 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran
𝑓)) |
109 | 108 | sseld 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
110 | 109 | anassrs 680 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
111 | 110 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
112 | 111 | expimpd 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
113 | 112 | impr 649 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
114 | 113 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
115 | | dfss3 3592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ⊆ (𝐺‘∪ ran
𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
116 | 114, 115 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran
𝑓)) |
117 | 28, 29, 30 | ttukeylem2 9332 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ((𝐺‘∪ ran
𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran
𝑓))) → 𝑤 ∈ 𝐴) |
118 | 56, 88, 116, 117 | syl12anc 1324 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴) |
119 | | 0ss 3972 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∅
⊆ 𝐵 |
120 | 28, 29, 30 | ttukeylem2 9332 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴) |
121 | 119, 120 | mpanr2 720 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴) |
122 | 29, 121 | mpdan 702 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∅ ∈ 𝐴) |
123 | 122 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴) |
124 | 55, 118, 123 | pm2.61ne 2879 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴) |
125 | 124 | expr 643 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴)) |
126 | 125 | exlimdv 1861 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴)) |
127 | 54, 126 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ 𝐴) |
128 | 127 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
→ 𝑤 ∈ 𝐴)) |
129 | 128 | ssrdv 3609 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴) |
130 | 28, 29, 30 | ttukeylem1 9331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ (𝐺
“ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴)) |
131 | 130 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺
“ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴)) |
132 | 129, 131 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺
“ 𝑦) ∈ 𝐴) |
133 | 132 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺
“ 𝑦) ∈ 𝐴) |
134 | 34, 133 | ifclda 4120 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴) |
135 | | uneq2 3761 |
. . . . . . . . . . . . . . 15
⊢ ({(𝐹‘∪ 𝑦)}
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) |
136 | 135 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ ({(𝐹‘∪ 𝑦)}
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)) |
137 | | un0 3967 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝑦)
∪ ∅) = (𝐺‘∪ 𝑦) |
138 | | uneq2 3761 |
. . . . . . . . . . . . . . . 16
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦)
∪ if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅))) |
139 | 137, 138 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) |
140 | 139 | eleq1d 2686 |
. . . . . . . . . . . . . 14
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)) |
141 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) |
142 | | vuniex 6954 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦
∈ V |
143 | 142 | sucid 5804 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑦
∈ suc ∪ 𝑦 |
144 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ On → Ord 𝑦) |
145 | | orduniorsuc 7030 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑦 → (𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦)) |
146 | 27, 144, 145 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦)) |
147 | 146 | orcanai 952 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦) |
148 | 143, 147 | syl5eleqr 2708 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦
∈ 𝑦) |
149 | | simplrr 801 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
150 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = ∪
𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦)) |
151 | 150 | eleq1d 2686 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ∪
𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴)) |
152 | 151 | rspcv 3305 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑦
∈ 𝑦 →
(∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘∪ 𝑦) ∈ 𝐴)) |
153 | 148, 149,
152 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴) |
154 | 153 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴) → (𝐺‘∪ 𝑦)
∈ 𝐴) |
155 | 136, 140,
141, 154 | ifbothda 4123 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴) |
156 | 134, 155 | ifclda 4120 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴) |
157 | 33, 156 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴) |
158 | 157 | expr 643 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴)) |
159 | 24, 158 | sylbird 250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)) |
160 | 159 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) →
(∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))) |
161 | 160 | com23 86 |
. . . . . . 7
⊢ (𝜑 → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
162 | 161 | a2i 14 |
. . . . . 6
⊢ ((𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
163 | 16, 162 | sylbi 207 |
. . . . 5
⊢
(∀𝑎 ∈
𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
164 | 163 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))) |
165 | 10, 15, 164 | tfis3 7057 |
. . 3
⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))) |
166 | 165 | impd 447 |
. 2
⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)) |
167 | 5, 166 | mpcom 38 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴) |