Step | Hyp | Ref
| Expression |
1 | | raleq 3138 |
. . . 4
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑)) |
2 | | feq2 6027 |
. . . . . 6
⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵)) |
3 | | raleq 3138 |
. . . . . 6
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓)) |
4 | 2, 3 | anbi12d 747 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
5 | 4 | exbidv 1850 |
. . . 4
⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
6 | 1, 5 | imbi12d 334 |
. . 3
⊢ (𝑢 = ∅ →
((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))) |
7 | | raleq 3138 |
. . . 4
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
8 | | feq2 6027 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵)) |
9 | | raleq 3138 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓)) |
10 | 8, 9 | anbi12d 747 |
. . . . 5
⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
11 | 10 | exbidv 1850 |
. . . 4
⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
12 | 7, 11 | imbi12d 334 |
. . 3
⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))) |
13 | | raleq 3138 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑)) |
14 | | feq2 6027 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵)) |
15 | | raleq 3138 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)) |
16 | 14, 15 | anbi12d 747 |
. . . . . 6
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
17 | 16 | exbidv 1850 |
. . . . 5
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
18 | | feq1 6026 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵)) |
19 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝑓‘𝑥) ∈ V |
20 | | ac6sfi.1 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) |
21 | 19, 20 | sbcie 3470 |
. . . . . . . . 9
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓) |
22 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
23 | 22 | sbceq1d 3440 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
24 | 21, 23 | syl5bbr 274 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
25 | 24 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
26 | 18, 25 | anbi12d 747 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
27 | 26 | cbvexv 2275 |
. . . . 5
⊢
(∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
28 | 17, 27 | syl6bb 276 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
29 | 13, 28 | imbi12d 334 |
. . 3
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
30 | | raleq 3138 |
. . . 4
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) |
31 | | feq2 6027 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵)) |
32 | | raleq 3138 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
33 | 31, 32 | anbi12d 747 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
34 | 33 | exbidv 1850 |
. . . 4
⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
35 | 30, 34 | imbi12d 334 |
. . 3
⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))) |
36 | | f0 6086 |
. . . 4
⊢
∅:∅⟶𝐵 |
37 | | 0ex 4790 |
. . . . 5
⊢ ∅
∈ V |
38 | | ral0 4076 |
. . . . . . 7
⊢
∀𝑥 ∈
∅ 𝜓 |
39 | 38 | biantru 526 |
. . . . . 6
⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
40 | | feq1 6026 |
. . . . . 6
⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔
∅:∅⟶𝐵)) |
41 | 39, 40 | syl5bbr 274 |
. . . . 5
⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵)) |
42 | 37, 41 | spcev 3300 |
. . . 4
⊢
(∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
43 | 36, 42 | mp1i 13 |
. . 3
⊢
(∀𝑥 ∈
∅ ∃𝑦 ∈
𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
44 | | ssun1 3776 |
. . . . . . 7
⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧}) |
45 | | ssralv 3666 |
. . . . . . 7
⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
46 | 44, 45 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑) |
47 | 46 | imim1i 63 |
. . . . 5
⊢
((∀𝑥 ∈
𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
48 | | ssun2 3777 |
. . . . . . . . 9
⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧}) |
49 | | ssralv 3666 |
. . . . . . . . 9
⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑) |
51 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
52 | | ralsnsg 4216 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
54 | | sbcrex 3514 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
55 | 53, 54 | bitri 264 |
. . . . . . . 8
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
56 | 50, 55 | sylib 208 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
57 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤 |
58 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) |
59 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵 |
60 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑤 ∪ {𝑧}) |
61 | | nfsbc1v 3455 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑 |
62 | 60, 61 | nfral 2945 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 |
63 | 59, 62 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
64 | 63 | nfex 2154 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
65 | 58, 64 | nfim 1825 |
. . . . . . . 8
⊢
Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
66 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵) |
67 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
68 | 51, 67 | f1osn 6176 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} |
69 | | f1of 6137 |
. . . . . . . . . . . . . . 15
⊢
({〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
70 | 68, 69 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
71 | | simpl2 1065 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵) |
72 | 71 | snssd 4340 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵) |
73 | 70, 72 | fssd 6057 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶𝐵) |
74 | | simpl1 1064 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤) |
75 | | disjsn 4246 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤) |
76 | 74, 75 | sylibr 224 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅) |
77 | | fun2 6067 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝑤⟶𝐵 ∧ {〈𝑧, 𝑦〉}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵) |
78 | 66, 73, 76, 77 | syl21anc 1325 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵) |
79 | | simprr 796 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓) |
80 | | eleq1a 2696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤)) |
81 | 80 | necon3bd 2808 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥)) |
82 | 81 | impcom 446 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥) |
83 | | fvunsn 6445 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥)) |
84 | | dfsbcq 3437 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
85 | 84, 21 | syl6rbb 277 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
86 | 82, 83, 85 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
87 | 86 | ralbidva 2985 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
88 | 74, 87 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
89 | 79, 88 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
90 | | simpl3 1066 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑) |
91 | | ffun 6048 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {〈𝑧, 𝑦〉})) |
92 | | ssun2 3777 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) |
93 | | vsnid 4209 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ {𝑧} |
94 | 67 | dmsnop 5609 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑧, 𝑦〉} = {𝑧} |
95 | 93, 94 | eleqtrri 2700 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ dom {〈𝑧, 𝑦〉} |
96 | | funssfv 6209 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ {〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ 𝑧 ∈ dom {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
97 | 92, 95, 96 | mp3an23 1416 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
98 | 78, 91, 97 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
99 | 51, 67 | fvsn 6446 |
. . . . . . . . . . . . . . . 16
⊢
({〈𝑧, 𝑦〉}‘𝑧) = 𝑦 |
100 | 98, 99 | syl6req 2673 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
101 | | ralsnsg 4216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
102 | 51, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
{𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑) |
103 | | elsni 4194 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧) |
104 | 103 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
105 | 104 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧))) |
106 | 105 | biimparc 504 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
107 | | sbceq1a 3446 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
109 | 108 | ralbidva 2985 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
110 | 102, 109 | syl5bbr 274 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
111 | 100, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
112 | 90, 111 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
113 | | ralun 3795 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
114 | 89, 112, 113 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
115 | | vex 3203 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
116 | | snex 4908 |
. . . . . . . . . . . . . 14
⊢
{〈𝑧, 𝑦〉} ∈
V |
117 | 115, 116 | unex 6956 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∈ V |
118 | | feq1 6026 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵)) |
119 | | fveq1 6190 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
120 | 119 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
121 | 120 | ralbidv 2986 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
122 | 118, 121 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑))) |
123 | 117, 122 | spcev 3300 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
124 | 78, 114, 123 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
125 | 124 | ex 450 |
. . . . . . . . . 10
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
126 | 125 | exlimdv 1861 |
. . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
127 | 126 | 3exp 1264 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))) |
128 | 57, 65, 127 | rexlimd 3026 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
129 | 56, 128 | syl5 34 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
130 | 129 | a2d 29 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
131 | 47, 130 | syl5 34 |
. . . 4
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
132 | 131 | adantl 482 |
. . 3
⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
133 | 6, 12, 29, 35, 43, 132 | findcard2s 8201 |
. 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
134 | 133 | imp 445 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |