Step | Hyp | Ref
| Expression |
1 | | raleq 2652 |
. . . 4
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑)) |
2 | | feq2 5303 |
. . . . . 6
⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵)) |
3 | | raleq 2652 |
. . . . . 6
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓)) |
4 | 2, 3 | anbi12d 465 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
5 | 4 | exbidv 1805 |
. . . 4
⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
6 | 1, 5 | imbi12d 233 |
. . 3
⊢ (𝑢 = ∅ →
((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))) |
7 | | raleq 2652 |
. . . 4
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
8 | | feq2 5303 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵)) |
9 | | raleq 2652 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓)) |
10 | 8, 9 | anbi12d 465 |
. . . . 5
⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
11 | 10 | exbidv 1805 |
. . . 4
⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
12 | 7, 11 | imbi12d 233 |
. . 3
⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))) |
13 | | raleq 2652 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑)) |
14 | | feq2 5303 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵)) |
15 | | raleq 2652 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)) |
16 | 14, 15 | anbi12d 465 |
. . . . . 6
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
17 | 16 | exbidv 1805 |
. . . . 5
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
18 | | feq1 5302 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵)) |
19 | | vex 2715 |
. . . . . . . . . . 11
⊢ 𝑓 ∈ V |
20 | | vex 2715 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
21 | 19, 20 | fvex 5488 |
. . . . . . . . . 10
⊢ (𝑓‘𝑥) ∈ V |
22 | | ac6sfi.1 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) |
23 | 21, 22 | sbcie 2971 |
. . . . . . . . 9
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓) |
24 | | fveq1 5467 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
25 | 24 | sbceq1d 2942 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
26 | 23, 25 | bitr3id 193 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
27 | 26 | ralbidv 2457 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
28 | 18, 27 | anbi12d 465 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
29 | 28 | cbvexv 1898 |
. . . . 5
⊢
(∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
30 | 17, 29 | bitrdi 195 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
31 | 13, 30 | imbi12d 233 |
. . 3
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
32 | | raleq 2652 |
. . . 4
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) |
33 | | feq2 5303 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵)) |
34 | | raleq 2652 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
35 | 33, 34 | anbi12d 465 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
36 | 35 | exbidv 1805 |
. . . 4
⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
37 | 32, 36 | imbi12d 233 |
. . 3
⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))) |
38 | | f0 5360 |
. . . 4
⊢
∅:∅⟶𝐵 |
39 | | 0ex 4091 |
. . . . 5
⊢ ∅
∈ V |
40 | | ral0 3495 |
. . . . . . 7
⊢
∀𝑥 ∈
∅ 𝜓 |
41 | 40 | biantru 300 |
. . . . . 6
⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
42 | | feq1 5302 |
. . . . . 6
⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔
∅:∅⟶𝐵)) |
43 | 41, 42 | bitr3id 193 |
. . . . 5
⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵)) |
44 | 39, 43 | spcev 2807 |
. . . 4
⊢
(∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
45 | 38, 44 | mp1i 10 |
. . 3
⊢
(∀𝑥 ∈
∅ ∃𝑦 ∈
𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
46 | | ssun1 3270 |
. . . . . . 7
⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧}) |
47 | | ssralv 3192 |
. . . . . . 7
⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑) |
49 | 48 | imim1i 60 |
. . . . 5
⊢
((∀𝑥 ∈
𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
50 | | ssun2 3271 |
. . . . . . . . 9
⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧}) |
51 | | ssralv 3192 |
. . . . . . . . 9
⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑) |
53 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
54 | | ralsnsg 3596 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
56 | | sbcrex 3016 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
57 | 55, 56 | bitri 183 |
. . . . . . . 8
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
58 | 52, 57 | sylib 121 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
59 | | nfv 1508 |
. . . . . . . 8
⊢
Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤 |
60 | | nfv 1508 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) |
61 | | nfv 1508 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵 |
62 | | nfcv 2299 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑤 ∪ {𝑧}) |
63 | | nfsbc1v 2955 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑 |
64 | 62, 63 | nfralxy 2495 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 |
65 | 61, 64 | nfan 1545 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
66 | 65 | nfex 1617 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
67 | 60, 66 | nfim 1552 |
. . . . . . . 8
⊢
Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
68 | | simprl 521 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵) |
69 | | vex 2715 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
70 | 53, 69 | f1osn 5454 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} |
71 | | f1of 5414 |
. . . . . . . . . . . . . . 15
⊢
({〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
72 | 70, 71 | mp1i 10 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
73 | | simpl2 986 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵) |
74 | 73 | snssd 3701 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵) |
75 | 72, 74 | fssd 5332 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶𝐵) |
76 | | simpl1 985 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤) |
77 | | disjsn 3621 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤) |
78 | 76, 77 | sylibr 133 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅) |
79 | | fun2 5343 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝑤⟶𝐵 ∧ {〈𝑧, 𝑦〉}:{𝑧}⟶𝐵) ∧ (𝑤 ∩ {𝑧}) = ∅) → (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵) |
80 | 68, 75, 78, 79 | syl21anc 1219 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵) |
81 | | simprr 522 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓) |
82 | | eleq1a 2229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤)) |
83 | 82 | necon3bd 2370 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥)) |
84 | 83 | impcom 124 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥) |
85 | | fvunsng 5661 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ V ∧ 𝑧 ≠ 𝑥) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥)) |
86 | 20, 85 | mpan 421 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥)) |
87 | | dfsbcq 2939 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
88 | 87, 23 | bitr2di 196 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
89 | 84, 86, 88 | 3syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
90 | 89 | ralbidva 2453 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
91 | 76, 90 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
92 | 81, 91 | mpbid 146 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
93 | | simpl3 987 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑) |
94 | | ffun 5322 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {〈𝑧, 𝑦〉})) |
95 | | ssun2 3271 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) |
96 | | vsnid 3592 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ {𝑧} |
97 | 69 | dmsnop 5059 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑧, 𝑦〉} = {𝑧} |
98 | 96, 97 | eleqtrri 2233 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ dom {〈𝑧, 𝑦〉} |
99 | | funssfv 5494 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ {〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ 𝑧 ∈ dom {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
100 | 95, 98, 99 | mp3an23 1311 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
101 | 80, 94, 100 | 3syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
102 | 53, 69 | fvsn 5662 |
. . . . . . . . . . . . . . . 16
⊢
({〈𝑧, 𝑦〉}‘𝑧) = 𝑦 |
103 | 101, 102 | eqtr2di 2207 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
104 | | ralsnsg 3596 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
105 | 53, 104 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
{𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑) |
106 | | elsni 3578 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧) |
107 | 106 | fveq2d 5472 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
108 | 107 | eqeq2d 2169 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧))) |
109 | 108 | biimparc 297 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
110 | | sbceq1a 2946 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
111 | 109, 110 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
112 | 111 | ralbidva 2453 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
113 | 105, 112 | bitr3id 193 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
114 | 103, 113 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
115 | 93, 114 | mpbid 146 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
116 | | ralun 3289 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
117 | 92, 115, 116 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
118 | 53, 69 | opex 4189 |
. . . . . . . . . . . . . . 15
⊢
〈𝑧, 𝑦〉 ∈ V |
119 | 118 | snex 4146 |
. . . . . . . . . . . . . 14
⊢
{〈𝑧, 𝑦〉} ∈
V |
120 | 19, 119 | unex 4401 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∈ V |
121 | | feq1 5302 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵)) |
122 | | fveq1 5467 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
123 | 122 | sbceq1d 2942 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
124 | 123 | ralbidv 2457 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
125 | 121, 124 | anbi12d 465 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑))) |
126 | 120, 125 | spcev 2807 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
127 | 80, 117, 126 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
128 | 127 | ex 114 |
. . . . . . . . . 10
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
129 | 128 | exlimdv 1799 |
. . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
130 | 129 | 3exp 1184 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))) |
131 | 59, 67, 130 | rexlimd 2571 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
132 | 58, 131 | syl5 32 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
133 | 132 | a2d 26 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
134 | 49, 133 | syl5 32 |
. . . 4
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
135 | 134 | adantl 275 |
. . 3
⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
136 | 6, 12, 31, 37, 45, 135 | findcard2s 6835 |
. 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
137 | 136 | imp 123 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |