| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . 5
⊢ 𝑤 ∈ V |
| 2 | | eleq2w2 2733 |
. . . . 5
⊢ (Fin = V
→ (𝑤 ∈ Fin ↔
𝑤 ∈
V)) |
| 3 | 1, 2 | mpbiri 258 |
. . . 4
⊢ (Fin = V
→ 𝑤 ∈
Fin) |
| 4 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅)) |
| 5 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅) |
| 6 | 5 | fneq2d 6662 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅)) |
| 7 | 4, 6 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))) |
| 8 | 7 | exbidv 1921 |
. . . . 5
⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))) |
| 9 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦)) |
| 10 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦) |
| 11 | 10 | fneq2d 6662 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦)) |
| 12 | 9, 11 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))) |
| 13 | 12 | exbidv 1921 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))) |
| 14 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧}))) |
| 15 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧})) |
| 16 | 15 | fneq2d 6662 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 17 | 14, 16 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
| 18 | 17 | exbidv 1921 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
| 19 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤)) |
| 20 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤) |
| 21 | 20 | fneq2d 6662 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤)) |
| 22 | 19, 21 | anbi12d 632 |
. . . . . 6
⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))) |
| 23 | 22 | exbidv 1921 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))) |
| 24 | | ssid 4006 |
. . . . . 6
⊢ ∅
⊆ ∅ |
| 25 | | fun0 6631 |
. . . . . . 7
⊢ Fun
∅ |
| 26 | | funfn 6596 |
. . . . . . 7
⊢ (Fun
∅ ↔ ∅ Fn dom ∅) |
| 27 | 25, 26 | mpbi 230 |
. . . . . 6
⊢ ∅
Fn dom ∅ |
| 28 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 29 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅
⊆ ∅)) |
| 30 | | fneq1 6659 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅
Fn dom ∅)) |
| 31 | 29, 30 | anbi12d 632 |
. . . . . . 7
⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅
⊆ ∅ ∧ ∅ Fn dom ∅))) |
| 32 | 28, 31 | spcev 3606 |
. . . . . 6
⊢ ((∅
⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)) |
| 33 | 24, 27, 32 | mp2an 692 |
. . . . 5
⊢
∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom
∅) |
| 34 | | sseq1 4009 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦)) |
| 35 | | fneq1 6659 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦)) |
| 36 | 34, 35 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))) |
| 37 | 36 | cbvexvw 2036 |
. . . . . . 7
⊢
(∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
| 38 | | ssun3 4180 |
. . . . . . . . . . 11
⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
| 40 | | dmun 5921 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧}) |
| 41 | | uneq2 4162 |
. . . . . . . . . . . . . . 15
⊢ (dom
{𝑧} = ∅ → (dom
𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅)) |
| 42 | | un0 4394 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑦 ∪ ∅) = dom
𝑦 |
| 43 | 41, 42 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (dom
{𝑧} = ∅ → (dom
𝑦 ∪ dom {𝑧}) = dom 𝑦) |
| 44 | 40, 43 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (dom
{𝑧} = ∅ → dom
(𝑦 ∪ {𝑧}) = dom 𝑦) |
| 45 | 44 | fneq2d 6662 |
. . . . . . . . . . . 12
⊢ (dom
{𝑧} = ∅ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom 𝑦)) |
| 46 | 45 | biimparc 479 |
. . . . . . . . . . 11
⊢ ((𝑔 Fn dom 𝑦 ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
| 47 | 46 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
| 48 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
| 49 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧}))) |
| 50 | | fneq1 6659 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
| 51 | 49, 50 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})))) |
| 52 | 48, 51 | spcev 3606 |
. . . . . . . . . 10
⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 53 | 39, 47, 52 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 54 | | dmsnn0 6227 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (V × V) ↔ dom
{𝑧} ≠
∅) |
| 55 | | elvv 5760 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (V × V) ↔
∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉) |
| 56 | 54, 55 | bitr3i 277 |
. . . . . . . . . . . 12
⊢ (dom
{𝑧} ≠ ∅ ↔
∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉) |
| 57 | 56 | anbi2i 623 |
. . . . . . . . . . 11
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉)) |
| 58 | | 19.42vv 1957 |
. . . . . . . . . . 11
⊢
(∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉)) |
| 59 | 57, 58 | bitr4i 278 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉)) |
| 60 | 38 | 3ad2ant1 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
| 61 | | snssi 4808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦) |
| 62 | | ssequn2 4189 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦) |
| 63 | 61, 62 | sylib 218 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦) |
| 64 | 63 | fneq2d 6662 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦)) |
| 65 | 64 | biimparc 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢})) |
| 66 | 65 | 3adant2 1132 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢})) |
| 67 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 〈𝑢, 𝑣〉 → {𝑧} = {〈𝑢, 𝑣〉}) |
| 68 | 67 | dmeqd 5916 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom {𝑧} = dom {〈𝑢, 𝑣〉}) |
| 69 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑣 ∈ V |
| 70 | 69 | dmsnop 6236 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom
{〈𝑢, 𝑣〉} = {𝑢} |
| 71 | 68, 70 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom {𝑧} = {𝑢}) |
| 72 | 71 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢})) |
| 73 | 40, 72 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢})) |
| 74 | 73 | fneq2d 6662 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢}))) |
| 75 | 74 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢}))) |
| 76 | 66, 75 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
| 77 | 76 | 3expia 1122 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
| 78 | 77 | 3adant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
| 79 | 60, 78, 52 | syl6an 684 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
| 80 | 67 | uneq2d 4168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {〈𝑢, 𝑣〉})) |
| 81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {〈𝑢, 𝑣〉})) |
| 82 | | unss1 4185 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
| 83 | 82 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
| 84 | 81, 83 | eqsstrrd 4019 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧})) |
| 85 | 84 | 3adant2 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧})) |
| 86 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑢 ∈ V |
| 87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑢 ∈ V) |
| 88 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑣 ∈ V) |
| 89 | | simpl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom 𝑦) |
| 90 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∪ {〈𝑢, 𝑣〉}) = (𝑔 ∪ {〈𝑢, 𝑣〉}) |
| 91 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢}) |
| 92 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦) |
| 93 | 87, 88, 89, 90, 91, 92 | fnunop 6684 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢})) |
| 94 | 93 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
| 95 | 94 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
| 96 | 73 | fneq2d 6662 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
| 97 | 96 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → ((𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
| 98 | 95, 97 | sylibrd 259 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}))) |
| 99 | | snex 5436 |
. . . . . . . . . . . . . . . 16
⊢
{〈𝑢, 𝑣〉} ∈
V |
| 100 | 48, 99 | unex 7764 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∪ {〈𝑢, 𝑣〉}) ∈ V |
| 101 | | sseq1 4009 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}))) |
| 102 | | fneq1 6659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}))) |
| 103 | 101, 102 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧})))) |
| 104 | 100, 103 | spcev 3606 |
. . . . . . . . . . . . . 14
⊢ (((𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 105 | 85, 98, 104 | syl6an 684 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
| 106 | 79, 105 | pm2.61d 179 |
. . . . . . . . . . . 12
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 107 | 106 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 108 | 107 | exlimivv 1932 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 109 | 59, 108 | sylbi 217 |
. . . . . . . . 9
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 110 | 53, 109 | pm2.61dane 3029 |
. . . . . . . 8
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 111 | 110 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 112 | 37, 111 | sylbi 217 |
. . . . . 6
⊢
(∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
| 113 | 112 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ Fin → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
| 114 | 8, 13, 18, 23, 33, 113 | findcard2 9204 |
. . . 4
⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
| 115 | 3, 114 | syl 17 |
. . 3
⊢ (Fin = V
→ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
| 116 | 115 | alrimiv 1927 |
. 2
⊢ (Fin = V
→ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
| 117 | | df-ac 10156 |
. 2
⊢
(CHOICE ↔ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
| 118 | 116, 117 | sylibr 234 |
1
⊢ (Fin = V
→ CHOICE) |