Step | Hyp | Ref
| Expression |
1 | | vex 3436 |
. . . . 5
⊢ 𝑤 ∈ V |
2 | | eleq2w2 2734 |
. . . . 5
⊢ (Fin = V
→ (𝑤 ∈ Fin ↔
𝑤 ∈
V)) |
3 | 1, 2 | mpbiri 257 |
. . . 4
⊢ (Fin = V
→ 𝑤 ∈
Fin) |
4 | | sseq2 3947 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ ∅)) |
5 | | dmeq 5812 |
. . . . . . . 8
⊢ (𝑥 = ∅ → dom 𝑥 = dom ∅) |
6 | 5 | fneq2d 6527 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom ∅)) |
7 | 4, 6 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))) |
8 | 7 | exbidv 1924 |
. . . . 5
⊢ (𝑥 = ∅ → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅))) |
9 | | sseq2 3947 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑦)) |
10 | | dmeq 5812 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → dom 𝑥 = dom 𝑦) |
11 | 10 | fneq2d 6527 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑦)) |
12 | 9, 11 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))) |
13 | 12 | exbidv 1924 |
. . . . 5
⊢ (𝑥 = 𝑦 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦))) |
14 | | sseq2 3947 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ (𝑦 ∪ {𝑧}))) |
15 | | dmeq 5812 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → dom 𝑥 = dom (𝑦 ∪ {𝑧})) |
16 | 15 | fneq2d 6527 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
17 | 14, 16 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
18 | 17 | exbidv 1924 |
. . . . 5
⊢ (𝑥 = (𝑦 ∪ {𝑧}) → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
19 | | sseq2 3947 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑓 ⊆ 𝑥 ↔ 𝑓 ⊆ 𝑤)) |
20 | | dmeq 5812 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → dom 𝑥 = dom 𝑤) |
21 | 20 | fneq2d 6527 |
. . . . . . 7
⊢ (𝑥 = 𝑤 → (𝑓 Fn dom 𝑥 ↔ 𝑓 Fn dom 𝑤)) |
22 | 19, 21 | anbi12d 631 |
. . . . . 6
⊢ (𝑥 = 𝑤 → ((𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ (𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))) |
23 | 22 | exbidv 1924 |
. . . . 5
⊢ (𝑥 = 𝑤 → (∃𝑓(𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥) ↔ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤))) |
24 | | ssid 3943 |
. . . . . 6
⊢ ∅
⊆ ∅ |
25 | | fun0 6499 |
. . . . . . 7
⊢ Fun
∅ |
26 | | funfn 6464 |
. . . . . . 7
⊢ (Fun
∅ ↔ ∅ Fn dom ∅) |
27 | 25, 26 | mpbi 229 |
. . . . . 6
⊢ ∅
Fn dom ∅ |
28 | | 0ex 5231 |
. . . . . . 7
⊢ ∅
∈ V |
29 | | sseq1 3946 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (𝑓 ⊆ ∅ ↔ ∅
⊆ ∅)) |
30 | | fneq1 6524 |
. . . . . . . 8
⊢ (𝑓 = ∅ → (𝑓 Fn dom ∅ ↔ ∅
Fn dom ∅)) |
31 | 29, 30 | anbi12d 631 |
. . . . . . 7
⊢ (𝑓 = ∅ → ((𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅) ↔ (∅
⊆ ∅ ∧ ∅ Fn dom ∅))) |
32 | 28, 31 | spcev 3545 |
. . . . . 6
⊢ ((∅
⊆ ∅ ∧ ∅ Fn dom ∅) → ∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom ∅)) |
33 | 24, 27, 32 | mp2an 689 |
. . . . 5
⊢
∃𝑓(𝑓 ⊆ ∅ ∧ 𝑓 Fn dom
∅) |
34 | | sseq1 3946 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓 ⊆ 𝑦 ↔ 𝑔 ⊆ 𝑦)) |
35 | | fneq1 6524 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → (𝑓 Fn dom 𝑦 ↔ 𝑔 Fn dom 𝑦)) |
36 | 34, 35 | anbi12d 631 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ (𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦))) |
37 | 36 | cbvexvw 2040 |
. . . . . . 7
⊢
(∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) ↔ ∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦)) |
38 | | ssun3 4108 |
. . . . . . . . . . 11
⊢ (𝑔 ⊆ 𝑦 → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
39 | 38 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
40 | | dmun 5819 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ dom {𝑧}) |
41 | | uneq2 4091 |
. . . . . . . . . . . . . . 15
⊢ (dom
{𝑧} = ∅ → (dom
𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ ∅)) |
42 | | un0 4324 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝑦 ∪ ∅) = dom
𝑦 |
43 | 41, 42 | eqtrdi 2794 |
. . . . . . . . . . . . . 14
⊢ (dom
{𝑧} = ∅ → (dom
𝑦 ∪ dom {𝑧}) = dom 𝑦) |
44 | 40, 43 | eqtrid 2790 |
. . . . . . . . . . . . 13
⊢ (dom
{𝑧} = ∅ → dom
(𝑦 ∪ {𝑧}) = dom 𝑦) |
45 | 44 | fneq2d 6527 |
. . . . . . . . . . . 12
⊢ (dom
{𝑧} = ∅ → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom 𝑦)) |
46 | 45 | biimparc 480 |
. . . . . . . . . . 11
⊢ ((𝑔 Fn dom 𝑦 ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
47 | 46 | adantll 711 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
48 | | vex 3436 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
49 | | sseq1 3946 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ 𝑔 ⊆ (𝑦 ∪ {𝑧}))) |
50 | | fneq1 6524 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑔 → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
51 | 49, 50 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑔 → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ (𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})))) |
52 | 48, 51 | spcev 3545 |
. . . . . . . . . 10
⊢ ((𝑔 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑔 Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
53 | 39, 47, 52 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} = ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
54 | | dmsnn0 6110 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (V × V) ↔ dom
{𝑧} ≠
∅) |
55 | | elvv 5661 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ (V × V) ↔
∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉) |
56 | 54, 55 | bitr3i 276 |
. . . . . . . . . . . 12
⊢ (dom
{𝑧} ≠ ∅ ↔
∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉) |
57 | 56 | anbi2i 623 |
. . . . . . . . . . 11
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉)) |
58 | | 19.42vv 1961 |
. . . . . . . . . . 11
⊢
(∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) ↔ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ ∃𝑢∃𝑣 𝑧 = 〈𝑢, 𝑣〉)) |
59 | 57, 58 | bitr4i 277 |
. . . . . . . . . 10
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) ↔ ∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉)) |
60 | 38 | 3ad2ant1 1132 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → 𝑔 ⊆ (𝑦 ∪ {𝑧})) |
61 | | snssi 4741 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ dom 𝑦 → {𝑢} ⊆ dom 𝑦) |
62 | | ssequn2 4117 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑢} ⊆ dom 𝑦 ↔ (dom 𝑦 ∪ {𝑢}) = dom 𝑦) |
63 | 61, 62 | sylib 217 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ dom 𝑦 → (dom 𝑦 ∪ {𝑢}) = dom 𝑦) |
64 | 63 | fneq2d 6527 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ dom 𝑦 → (𝑔 Fn (dom 𝑦 ∪ {𝑢}) ↔ 𝑔 Fn dom 𝑦)) |
65 | 64 | biimparc 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢})) |
66 | 65 | 3adant2 1130 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn (dom 𝑦 ∪ {𝑢})) |
67 | | sneq 4571 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 〈𝑢, 𝑣〉 → {𝑧} = {〈𝑢, 𝑣〉}) |
68 | 67 | dmeqd 5814 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom {𝑧} = dom {〈𝑢, 𝑣〉}) |
69 | | vex 3436 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑣 ∈ V |
70 | 69 | dmsnop 6119 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ dom
{〈𝑢, 𝑣〉} = {𝑢} |
71 | 68, 70 | eqtrdi 2794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom {𝑧} = {𝑢}) |
72 | 71 | uneq2d 4097 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (dom 𝑦 ∪ dom {𝑧}) = (dom 𝑦 ∪ {𝑢})) |
73 | 40, 72 | eqtrid 2790 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = 〈𝑢, 𝑣〉 → dom (𝑦 ∪ {𝑧}) = (dom 𝑦 ∪ {𝑢})) |
74 | 73 | fneq2d 6527 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢}))) |
75 | 74 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → (𝑔 Fn dom (𝑦 ∪ {𝑧}) ↔ 𝑔 Fn (dom 𝑦 ∪ {𝑢}))) |
76 | 66, 75 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom (𝑦 ∪ {𝑧})) |
77 | 76 | 3expia 1120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
78 | 77 | 3adant1 1129 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → 𝑔 Fn dom (𝑦 ∪ {𝑧}))) |
79 | 60, 78, 52 | syl6an 681 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
80 | 67 | uneq2d 4097 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {〈𝑢, 𝑣〉})) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {𝑧}) = (𝑔 ∪ {〈𝑢, 𝑣〉})) |
82 | | unss1 4113 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ⊆ 𝑦 → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {𝑧}) ⊆ (𝑦 ∪ {𝑧})) |
84 | 81, 83 | eqsstrrd 3960 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧})) |
85 | 84 | 3adant2 1130 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧})) |
86 | | vex 3436 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑢 ∈ V |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑢 ∈ V) |
88 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑣 ∈ V) |
89 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → 𝑔 Fn dom 𝑦) |
90 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 ∪ {〈𝑢, 𝑣〉}) = (𝑔 ∪ {〈𝑢, 𝑣〉}) |
91 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢ (dom
𝑦 ∪ {𝑢}) = (dom 𝑦 ∪ {𝑢}) |
92 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → ¬ 𝑢 ∈ dom 𝑦) |
93 | 87, 88, 89, 90, 91, 92 | fnunop 6547 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 Fn dom 𝑦 ∧ ¬ 𝑢 ∈ dom 𝑦) → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢})) |
94 | 93 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 Fn dom 𝑦 → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
95 | 94 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
96 | 73 | fneq2d 6527 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑢, 𝑣〉 → ((𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
97 | 96 | 3ad2ant3 1134 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → ((𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn (dom 𝑦 ∪ {𝑢}))) |
98 | 95, 97 | sylibrd 258 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}))) |
99 | | snex 5354 |
. . . . . . . . . . . . . . . 16
⊢
{〈𝑢, 𝑣〉} ∈
V |
100 | 48, 99 | unex 7596 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∪ {〈𝑢, 𝑣〉}) ∈ V |
101 | | sseq1 3946 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → (𝑓 ⊆ (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}))) |
102 | | fneq1 6524 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → (𝑓 Fn dom (𝑦 ∪ {𝑧}) ↔ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧}))) |
103 | 101, 102 | anbi12d 631 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑔 ∪ {〈𝑢, 𝑣〉}) → ((𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})) ↔ ((𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧})))) |
104 | 100, 103 | spcev 3545 |
. . . . . . . . . . . . . 14
⊢ (((𝑔 ∪ {〈𝑢, 𝑣〉}) ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑔 ∪ {〈𝑢, 𝑣〉}) Fn dom (𝑦 ∪ {𝑧})) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
105 | 85, 98, 104 | syl6an 681 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → (¬ 𝑢 ∈ dom 𝑦 → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
106 | 79, 105 | pm2.61d 179 |
. . . . . . . . . . . 12
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦 ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
107 | 106 | 3expa 1117 |
. . . . . . . . . . 11
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
108 | 107 | exlimivv 1935 |
. . . . . . . . . 10
⊢
(∃𝑢∃𝑣((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ 𝑧 = 〈𝑢, 𝑣〉) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
109 | 59, 108 | sylbi 216 |
. . . . . . . . 9
⊢ (((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) ∧ dom {𝑧} ≠ ∅) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
110 | 53, 109 | pm2.61dane 3032 |
. . . . . . . 8
⊢ ((𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
111 | 110 | exlimiv 1933 |
. . . . . . 7
⊢
(∃𝑔(𝑔 ⊆ 𝑦 ∧ 𝑔 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
112 | 37, 111 | sylbi 216 |
. . . . . 6
⊢
(∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧}))) |
113 | 112 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ Fin → (∃𝑓(𝑓 ⊆ 𝑦 ∧ 𝑓 Fn dom 𝑦) → ∃𝑓(𝑓 ⊆ (𝑦 ∪ {𝑧}) ∧ 𝑓 Fn dom (𝑦 ∪ {𝑧})))) |
114 | 8, 13, 18, 23, 33, 113 | findcard2 8947 |
. . . 4
⊢ (𝑤 ∈ Fin → ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
115 | 3, 114 | syl 17 |
. . 3
⊢ (Fin = V
→ ∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
116 | 115 | alrimiv 1930 |
. 2
⊢ (Fin = V
→ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
117 | | df-ac 9872 |
. 2
⊢
(CHOICE ↔ ∀𝑤∃𝑓(𝑓 ⊆ 𝑤 ∧ 𝑓 Fn dom 𝑤)) |
118 | 116, 117 | sylibr 233 |
1
⊢ (Fin = V
→ CHOICE) |