| Step | Hyp | Ref
| Expression |
| 1 | | raleq 3323 |
. . . 4
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑)) |
| 2 | | feq2 6717 |
. . . . . 6
⊢ (𝑢 = ∅ → (𝑓:𝑢⟶𝐵 ↔ 𝑓:∅⟶𝐵)) |
| 3 | | raleq 3323 |
. . . . . 6
⊢ (𝑢 = ∅ → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ ∅ 𝜓)) |
| 4 | 2, 3 | anbi12d 632 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
| 5 | 4 | exbidv 1921 |
. . . 4
⊢ (𝑢 = ∅ → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓))) |
| 6 | 1, 5 | imbi12d 344 |
. . 3
⊢ (𝑢 = ∅ →
((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ ∅ ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)))) |
| 7 | | raleq 3323 |
. . . 4
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
| 8 | | feq2 6717 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝑤⟶𝐵)) |
| 9 | | raleq 3323 |
. . . . . 6
⊢ (𝑢 = 𝑤 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝑤 𝜓)) |
| 10 | 8, 9 | anbi12d 632 |
. . . . 5
⊢ (𝑢 = 𝑤 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
| 11 | 10 | exbidv 1921 |
. . . 4
⊢ (𝑢 = 𝑤 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
| 12 | 7, 11 | imbi12d 344 |
. . 3
⊢ (𝑢 = 𝑤 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)))) |
| 13 | | raleq 3323 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑)) |
| 14 | | feq2 6717 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (𝑓:𝑢⟶𝐵 ↔ 𝑓:(𝑤 ∪ {𝑧})⟶𝐵)) |
| 15 | | raleq 3323 |
. . . . . . 7
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓)) |
| 16 | 14, 15 | anbi12d 632 |
. . . . . 6
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
| 17 | 16 | exbidv 1921 |
. . . . 5
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓))) |
| 18 | | feq1 6716 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ↔ 𝑔:(𝑤 ∪ {𝑧})⟶𝐵)) |
| 19 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑓‘𝑥) ∈ V |
| 20 | | ac6sfi.1 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) |
| 21 | 19, 20 | sbcie 3830 |
. . . . . . . . 9
⊢
([(𝑓‘𝑥) / 𝑦]𝜑 ↔ 𝜓) |
| 22 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑔 → (𝑓‘𝑥) = (𝑔‘𝑥)) |
| 23 | 22 | sbceq1d 3793 |
. . . . . . . . 9
⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
| 24 | 21, 23 | bitr3id 285 |
. . . . . . . 8
⊢ (𝑓 = 𝑔 → (𝜓 ↔ [(𝑔‘𝑥) / 𝑦]𝜑)) |
| 25 | 24 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑓 = 𝑔 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
| 26 | 18, 25 | anbi12d 632 |
. . . . . 6
⊢ (𝑓 = 𝑔 → ((𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
| 27 | 26 | cbvexvw 2036 |
. . . . 5
⊢
(∃𝑓(𝑓:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
| 28 | 17, 27 | bitrdi 287 |
. . . 4
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
| 29 | 13, 28 | imbi12d 344 |
. . 3
⊢ (𝑢 = (𝑤 ∪ {𝑧}) → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 30 | | raleq 3323 |
. . . 4
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑)) |
| 31 | | feq2 6717 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑓:𝑢⟶𝐵 ↔ 𝑓:𝐴⟶𝐵)) |
| 32 | | raleq 3323 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (∀𝑥 ∈ 𝑢 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜓)) |
| 33 | 31, 32 | anbi12d 632 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
| 34 | 33 | exbidv 1921 |
. . . 4
⊢ (𝑢 = 𝐴 → (∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓) ↔ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
| 35 | 30, 34 | imbi12d 344 |
. . 3
⊢ (𝑢 = 𝐴 → ((∀𝑥 ∈ 𝑢 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑢⟶𝐵 ∧ ∀𝑥 ∈ 𝑢 𝜓)) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)))) |
| 36 | | f0 6789 |
. . . 4
⊢
∅:∅⟶𝐵 |
| 37 | | 0ex 5307 |
. . . . 5
⊢ ∅
∈ V |
| 38 | | ral0 4513 |
. . . . . . 7
⊢
∀𝑥 ∈
∅ 𝜓 |
| 39 | 38 | biantru 529 |
. . . . . 6
⊢ (𝑓:∅⟶𝐵 ↔ (𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
| 40 | | feq1 6716 |
. . . . . 6
⊢ (𝑓 = ∅ → (𝑓:∅⟶𝐵 ↔
∅:∅⟶𝐵)) |
| 41 | 39, 40 | bitr3id 285 |
. . . . 5
⊢ (𝑓 = ∅ → ((𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓) ↔ ∅:∅⟶𝐵)) |
| 42 | 37, 41 | spcev 3606 |
. . . 4
⊢
(∅:∅⟶𝐵 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
| 43 | 36, 42 | mp1i 13 |
. . 3
⊢
(∀𝑥 ∈
∅ ∃𝑦 ∈
𝐵 𝜑 → ∃𝑓(𝑓:∅⟶𝐵 ∧ ∀𝑥 ∈ ∅ 𝜓)) |
| 44 | | ssun1 4178 |
. . . . . . 7
⊢ 𝑤 ⊆ (𝑤 ∪ {𝑧}) |
| 45 | | ssralv 4052 |
. . . . . . 7
⊢ (𝑤 ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑)) |
| 46 | 44, 45 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑) |
| 47 | 46 | imim1i 63 |
. . . . 5
⊢
((∀𝑥 ∈
𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓))) |
| 48 | | ssun2 4179 |
. . . . . . . . 9
⊢ {𝑧} ⊆ (𝑤 ∪ {𝑧}) |
| 49 | | ssralv 4052 |
. . . . . . . . 9
⊢ ({𝑧} ⊆ (𝑤 ∪ {𝑧}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑)) |
| 50 | 48, 49 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑) |
| 51 | | ralsnsg 4670 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑)) |
| 52 | 51 | elv 3485 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑) |
| 53 | | sbcrex 3875 |
. . . . . . . . 9
⊢
([𝑧 / 𝑥]∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
| 54 | 52, 53 | bitri 275 |
. . . . . . . 8
⊢
(∀𝑥 ∈
{𝑧}∃𝑦 ∈ 𝐵 𝜑 ↔ ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
| 55 | 50, 54 | sylib 218 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
| 56 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦 ¬ 𝑧 ∈ 𝑤 |
| 57 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) |
| 58 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦 𝑔:(𝑤 ∪ {𝑧})⟶𝐵 |
| 59 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(𝑤 ∪ {𝑧}) |
| 60 | | nfsbc1v 3808 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦[(𝑔‘𝑥) / 𝑦]𝜑 |
| 61 | 59, 60 | nfralw 3311 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 |
| 62 | 58, 61 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
| 63 | 62 | nfex 2324 |
. . . . . . . . 9
⊢
Ⅎ𝑦∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) |
| 64 | 57, 63 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑦(∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
| 65 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑓:𝑤⟶𝐵) |
| 66 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑧 ∈ V |
| 67 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
| 68 | 66, 67 | f1osn 6888 |
. . . . . . . . . . . . . . 15
⊢
{〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} |
| 69 | | f1of 6848 |
. . . . . . . . . . . . . . 15
⊢
({〈𝑧, 𝑦〉}:{𝑧}–1-1-onto→{𝑦} → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
| 70 | 68, 69 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶{𝑦}) |
| 71 | | simpl2 1193 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 ∈ 𝐵) |
| 72 | 71 | snssd 4809 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {𝑦} ⊆ 𝐵) |
| 73 | 70, 72 | fssd 6753 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → {〈𝑧, 𝑦〉}:{𝑧}⟶𝐵) |
| 74 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ¬ 𝑧 ∈ 𝑤) |
| 75 | | disjsn 4711 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑤) |
| 76 | 74, 75 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑤 ∩ {𝑧}) = ∅) |
| 77 | 65, 73, 76 | fun2d 6772 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵) |
| 78 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 𝜓) |
| 79 | | eleq1a 2836 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑤 → (𝑧 = 𝑥 → 𝑧 ∈ 𝑤)) |
| 80 | 79 | necon3bd 2954 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑤 → (¬ 𝑧 ∈ 𝑤 → 𝑧 ≠ 𝑥)) |
| 81 | 80 | impcom 407 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → 𝑧 ≠ 𝑥) |
| 82 | | fvunsn 7199 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ≠ 𝑥 → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥)) |
| 83 | | dfsbcq 3790 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → ([((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 84 | 83, 21 | bitr2di 288 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = (𝑓‘𝑥) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 85 | 81, 82, 84 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑤) → (𝜓 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 86 | 85 | ralbidva 3176 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 87 | 74, 86 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ 𝑤 𝜓 ↔ ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 88 | 78, 87 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ 𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
| 89 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → [𝑧 / 𝑥]𝜑) |
| 90 | | ffun 6739 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 → Fun (𝑓 ∪ {〈𝑧, 𝑦〉})) |
| 91 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . 18
⊢
{〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) |
| 92 | | vsnid 4663 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑧 ∈ {𝑧} |
| 93 | 67 | dmsnop 6236 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
{〈𝑧, 𝑦〉} = {𝑧} |
| 94 | 92, 93 | eleqtrri 2840 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ dom {〈𝑧, 𝑦〉} |
| 95 | | funssfv 6927 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ {〈𝑧, 𝑦〉} ⊆ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∧ 𝑧 ∈ dom {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
| 96 | 91, 94, 95 | mp3an23 1455 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
(𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
| 97 | 77, 90, 96 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
| 98 | 66, 67 | fvsn 7201 |
. . . . . . . . . . . . . . . 16
⊢
({〈𝑧, 𝑦〉}‘𝑧) = 𝑦 |
| 99 | 97, 98 | eqtr2di 2794 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
| 100 | | ralsnsg 4670 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ V → (∀𝑥 ∈ {𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
| 101 | 100 | elv 3485 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑥 ∈
{𝑧}𝜑 ↔ [𝑧 / 𝑥]𝜑) |
| 102 | | elsni 4643 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ {𝑧} → 𝑥 = 𝑧) |
| 103 | 102 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑧} → ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧)) |
| 104 | 103 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {𝑧} → (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) ↔ 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧))) |
| 105 | 104 | biimparc 479 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → 𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
| 106 | | sbceq1a 3799 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) ∧ 𝑥 ∈ {𝑧}) → (𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 108 | 107 | ralbidva 3176 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → (∀𝑥 ∈ {𝑧}𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 109 | 101, 108 | bitr3id 285 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑧) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 110 | 99, 109 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ([𝑧 / 𝑥]𝜑 ↔ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 111 | 89, 110 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
| 112 | | ralun 4198 |
. . . . . . . . . . . . 13
⊢
((∀𝑥 ∈
𝑤 [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑 ∧ ∀𝑥 ∈ {𝑧}[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
| 113 | 88, 111, 112 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) |
| 114 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
| 115 | | snex 5436 |
. . . . . . . . . . . . . 14
⊢
{〈𝑧, 𝑦〉} ∈
V |
| 116 | 114, 115 | unex 7764 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∪ {〈𝑧, 𝑦〉}) ∈ V |
| 117 | | feq1 6716 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ↔ (𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵)) |
| 118 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (𝑔‘𝑥) = ((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥)) |
| 119 | 118 | sbceq1d 3793 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ([(𝑔‘𝑥) / 𝑦]𝜑 ↔ [((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 120 | 119 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑 ↔ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑)) |
| 121 | 117, 120 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑓 ∪ {〈𝑧, 𝑦〉}) → ((𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑) ↔ ((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑))) |
| 122 | 116, 121 | spcev 3606 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∪ {〈𝑧, 𝑦〉}):(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[((𝑓 ∪ {〈𝑧, 𝑦〉})‘𝑥) / 𝑦]𝜑) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
| 123 | 77, 113, 122 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) ∧ (𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)) |
| 124 | 123 | ex 412 |
. . . . . . . . . 10
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → ((𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
| 125 | 124 | exlimdv 1933 |
. . . . . . . . 9
⊢ ((¬
𝑧 ∈ 𝑤 ∧ 𝑦 ∈ 𝐵 ∧ [𝑧 / 𝑥]𝜑) → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))) |
| 126 | 125 | 3exp 1120 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝑤 → (𝑦 ∈ 𝐵 → ([𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑))))) |
| 127 | 56, 64, 126 | rexlimd 3266 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝑤 → (∃𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 128 | 55, 127 | syl5 34 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑤 → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → (∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓) → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 129 | 128 | a2d 29 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 130 | 47, 129 | syl5 34 |
. . . 4
⊢ (¬
𝑧 ∈ 𝑤 → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 131 | 130 | adantl 481 |
. . 3
⊢ ((𝑤 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑤) → ((∀𝑥 ∈ 𝑤 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝑤⟶𝐵 ∧ ∀𝑥 ∈ 𝑤 𝜓)) → (∀𝑥 ∈ (𝑤 ∪ {𝑧})∃𝑦 ∈ 𝐵 𝜑 → ∃𝑔(𝑔:(𝑤 ∪ {𝑧})⟶𝐵 ∧ ∀𝑥 ∈ (𝑤 ∪ {𝑧})[(𝑔‘𝑥) / 𝑦]𝜑)))) |
| 132 | 6, 12, 29, 35, 43, 131 | findcard2s 9205 |
. 2
⊢ (𝐴 ∈ Fin →
(∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓))) |
| 133 | 132 | imp 406 |
1
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 𝜓)) |