Step | Hyp | Ref
| Expression |
1 | | cardon 9560 |
. . . . 5
⊢
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On |
2 | 1 | onsuci 7617 |
. . . 4
⊢ suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → suc (card‘(∪ 𝐴
∖ 𝐵)) ∈
On) |
4 | | onelon 6238 |
. . 3
⊢ ((suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝐶 ∈ On) |
5 | 3, 4 | sylan 583 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝐶 ∈ On) |
6 | | eleq1 2825 |
. . . . . 6
⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)))) |
7 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎)) |
8 | 7 | eleq1d 2822 |
. . . . . 6
⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴)) |
9 | 6, 8 | imbi12d 348 |
. . . . 5
⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
10 | 9 | imbi2d 344 |
. . . 4
⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))) |
11 | | eleq1 2825 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)))) |
12 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶)) |
13 | 12 | eleq1d 2822 |
. . . . . 6
⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴)) |
14 | 11, 13 | imbi12d 348 |
. . . . 5
⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))) |
15 | 14 | imbi2d 344 |
. . . 4
⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))) |
16 | | r19.21v 3098 |
. . . . . 6
⊢
(∀𝑎 ∈
𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
17 | 2 | onordi 6318 |
. . . . . . . . . . . . . . 15
⊢ Ord suc
(card‘(∪ 𝐴 ∖ 𝐵)) |
18 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Ord suc (card‘(∪ 𝐴
∖ 𝐵))) |
19 | | ordelss 6229 |
. . . . . . . . . . . . . 14
⊢ ((Ord suc
(card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴
∖ 𝐵))) |
20 | 18, 19 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴
∖ 𝐵))) |
21 | 20 | sselda 3901 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → 𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) |
22 | | biimt 364 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
24 | 23 | ralbidva 3117 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))) |
25 | 2 | onssi 7616 |
. . . . . . . . . . . . . 14
⊢ suc
(card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On |
26 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) |
27 | 25, 26 | sselid 3898 |
. . . . . . . . . . . . 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 10125 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) |
33 | 27, 32 | syldan 594 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) |
34 | 29 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴) |
35 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ (𝒫
∪ (𝐺 “ 𝑦) ∩ Fin)) |
36 | 35 | elin2d 4113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈
Fin) |
37 | 35 | elin1d 4112 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ 𝒫
∪ (𝐺 “ 𝑦)) |
38 | 37 | elpwid 4524 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ⊆ ∪ (𝐺
“ 𝑦)) |
39 | 31 | tfr1 8133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐺 Fn On |
40 | | fnfun 6479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺 Fn On → Fun 𝐺) |
41 | | funiunfv 7061 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)) |
42 | 39, 40, 41 | mp2b 10 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦) |
43 | 38, 42 | sseqtrrdi 3952 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣)) |
44 | | dfss3 3888 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪
𝑣 ∈ 𝑦 (𝐺‘𝑣)) |
45 | | eliun 4908 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
46 | 45 | ralbii 3088 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑢 ∈
𝑤 𝑢 ∈ ∪
𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
47 | 44, 46 | bitri 278 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
48 | 43, 47 | sylib 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ∀𝑢 ∈
𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) |
49 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢))) |
50 | 49 | eleq2d 2823 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
51 | 50 | ac6sfi 8915 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
52 | 36, 48, 51 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)))) |
53 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
54 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑) |
55 | | fveq2 6717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = ∪
ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran
𝑓)) |
56 | 55 | eleq1d 2822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = ∪
ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran
𝑓) ∈ 𝐴)) |
57 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
58 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
59 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦) |
60 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦) |
61 | | frn 6552 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦) |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦) |
63 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On) |
64 | | onss 7568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑦 ∈ On → 𝑦 ⊆ On) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On) |
66 | 62, 65 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On) |
67 | 36 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin) |
68 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin) |
69 | | ffn 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤) |
70 | 60, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤) |
71 | | dffn4 6639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓) |
72 | 70, 71 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓) |
73 | | fofi 8962 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
74 | 68, 72, 73 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin) |
75 | | dm0rn0 5794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) |
76 | 59 | fdmd 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤) |
77 | 76 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅)) |
78 | 75, 77 | bitr3id 288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅)) |
79 | 78 | necon3bid 2985 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
80 | 79 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅) |
81 | | ordunifi 8921 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ran
𝑓 ⊆ On ∧ ran
𝑓 ∈ Fin ∧ ran
𝑓 ≠ ∅) →
∪ ran 𝑓 ∈ ran 𝑓) |
82 | 66, 74, 80, 81 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓) |
83 | 62, 82 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦) |
84 | 56, 58, 83 | rspcdva 3539 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran
𝑓) ∈ 𝐴) |
85 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑) |
86 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On) |
87 | 86, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On) |
88 | | ffvelrn 6902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦) |
89 | 88 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦) |
90 | 87, 89 | sseldd 3902 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On) |
91 | 61 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦) |
92 | 91, 87 | sstrd 3911 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On) |
93 | | vex 3412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ 𝑓 ∈ V |
94 | 93 | rnex 7690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ran 𝑓 ∈ V |
95 | 94 | ssonunii 7565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (ran
𝑓 ⊆ On → ∪ ran 𝑓 ∈ On) |
96 | 92, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran
𝑓 ∈
On) |
97 | 69 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤) |
98 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤) |
99 | | fnfvelrn 6901 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓) |
100 | 97, 98, 99 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓) |
101 | | elssuni 4851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran
𝑓) |
102 | 100, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran
𝑓) |
103 | 28, 29, 30, 31 | ttukeylem5 10127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran
𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran
𝑓)) |
104 | 85, 90, 96, 102, 103 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran
𝑓)) |
105 | 104 | sseld 3900 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
106 | 105 | anassrs 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
107 | 106 | ralimdva 3100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
108 | 107 | expimpd 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓))) |
109 | 108 | impr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
110 | 109 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
111 | | dfss3 3888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ⊆ (𝐺‘∪ ran
𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran
𝑓)) |
112 | 110, 111 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran
𝑓)) |
113 | 28, 29, 30 | ttukeylem2 10124 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ ((𝐺‘∪ ran
𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran
𝑓))) → 𝑤 ∈ 𝐴) |
114 | 54, 84, 112, 113 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴) |
115 | | 0ss 4311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ∅
⊆ 𝐵 |
116 | 28, 29, 30 | ttukeylem2 10124 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴) |
117 | 115, 116 | mpanr2 704 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴) |
118 | 29, 117 | mpdan 687 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∅ ∈ 𝐴) |
119 | 118 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴) |
120 | 53, 114, 119 | pm2.61ne 3027 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin) ∧
(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴) |
121 | 120 | expr 460 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴)) |
122 | 121 | exlimdv 1941 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴)) |
123 | 52, 122 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin))
→ 𝑤 ∈ 𝐴) |
124 | 123 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
→ 𝑤 ∈ 𝐴)) |
125 | 124 | ssrdv 3907 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴) |
126 | 28, 29, 30 | ttukeylem1 10123 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∪ (𝐺
“ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴)) |
127 | 126 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺
“ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺
“ 𝑦) ∩ Fin)
⊆ 𝐴)) |
128 | 125, 127 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺
“ 𝑦) ∈ 𝐴) |
129 | 128 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺
“ 𝑦) ∈ 𝐴) |
130 | 34, 129 | ifclda 4474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴) |
131 | | uneq2 4071 |
. . . . . . . . . . . . . . 15
⊢ ({(𝐹‘∪ 𝑦)}
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) |
132 | 131 | eleq1d 2822 |
. . . . . . . . . . . . . 14
⊢ ({(𝐹‘∪ 𝑦)}
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)) |
133 | | un0 4305 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘∪ 𝑦)
∪ ∅) = (𝐺‘∪ 𝑦) |
134 | | uneq2 4071 |
. . . . . . . . . . . . . . . 16
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦)
∪ if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅))) |
135 | 133, 134 | eqtr3id 2792 |
. . . . . . . . . . . . . . 15
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) |
136 | 135 | eleq1d 2822 |
. . . . . . . . . . . . . 14
⊢ (∅
= if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)) |
137 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) |
138 | | fveq2 6717 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ∪
𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦)) |
139 | 138 | eleq1d 2822 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = ∪
𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴)) |
140 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴) |
141 | | vuniex 7527 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦
∈ V |
142 | 141 | sucid 6292 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑦
∈ suc ∪ 𝑦 |
143 | | eloni 6223 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ On → Ord 𝑦) |
144 | | orduniorsuc 7609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑦 → (𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦)) |
145 | 27, 143, 144 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦)) |
146 | 145 | orcanai 1003 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦) |
147 | 142, 146 | eleqtrrid 2845 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦
∈ 𝑦) |
148 | 139, 140,
147 | rspcdva 3539 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴) |
149 | 148 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴) → (𝐺‘∪ 𝑦)
∈ 𝐴) |
150 | 132, 136,
137, 149 | ifbothda 4477 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴) |
151 | 130, 150 | ifclda 4474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴) |
152 | 33, 151 | eqeltrd 2838 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) ∧
∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴) |
153 | 152 | expr 460 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴)) |
154 | 24, 153 | sylbird 263 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) →
(∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)) |
155 | 154 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) →
(∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))) |
156 | 155 | com23 86 |
. . . . . . 7
⊢ (𝜑 → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
157 | 156 | a2i 14 |
. . . . . 6
⊢ ((𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
158 | 16, 157 | sylbi 220 |
. . . . 5
⊢
(∀𝑎 ∈
𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))) |
159 | 158 | a1i 11 |
. . . 4
⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))) |
160 | 10, 15, 159 | tfis3 7636 |
. . 3
⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))) |
161 | 160 | impd 414 |
. 2
⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)) |
162 | 5, 161 | mpcom 38 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴
∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴) |