Step | Hyp | Ref
| Expression |
1 | | sneq 3592 |
. . . 4
⊢ (𝑧 = 𝐴 → {𝑧} = {𝐴}) |
2 | 1 | ixpeq1d 6684 |
. . 3
⊢ (𝑧 = 𝐴 → X𝑥 ∈ {𝑧}𝐵 = X𝑥 ∈ {𝐴}𝐵) |
3 | 2 | eleq2d 2240 |
. 2
⊢ (𝑧 = 𝐴 → (𝐹 ∈ X𝑥 ∈ {𝑧}𝐵 ↔ 𝐹 ∈ X𝑥 ∈ {𝐴}𝐵)) |
4 | | opeq1 3763 |
. . . . 5
⊢ (𝑧 = 𝐴 → 〈𝑧, 𝑦〉 = 〈𝐴, 𝑦〉) |
5 | 4 | sneqd 3594 |
. . . 4
⊢ (𝑧 = 𝐴 → {〈𝑧, 𝑦〉} = {〈𝐴, 𝑦〉}) |
6 | 5 | eqeq2d 2182 |
. . 3
⊢ (𝑧 = 𝐴 → (𝐹 = {〈𝑧, 𝑦〉} ↔ 𝐹 = {〈𝐴, 𝑦〉})) |
7 | 6 | rexbidv 2471 |
. 2
⊢ (𝑧 = 𝐴 → (∃𝑦 ∈ 𝐵 𝐹 = {〈𝑧, 𝑦〉} ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) |
8 | | elex 2741 |
. . 3
⊢ (𝐹 ∈ X𝑥 ∈
{𝑧}𝐵 → 𝐹 ∈ V) |
9 | | vex 2733 |
. . . . . . 7
⊢ 𝑧 ∈ V |
10 | | vex 2733 |
. . . . . . 7
⊢ 𝑦 ∈ V |
11 | 9, 10 | opex 4212 |
. . . . . 6
⊢
〈𝑧, 𝑦〉 ∈ V |
12 | 11 | snex 4169 |
. . . . 5
⊢
{〈𝑧, 𝑦〉} ∈
V |
13 | | eleq1 2233 |
. . . . 5
⊢ (𝐹 = {〈𝑧, 𝑦〉} → (𝐹 ∈ V ↔ {〈𝑧, 𝑦〉} ∈ V)) |
14 | 12, 13 | mpbiri 167 |
. . . 4
⊢ (𝐹 = {〈𝑧, 𝑦〉} → 𝐹 ∈ V) |
15 | 14 | rexlimivw 2583 |
. . 3
⊢
(∃𝑦 ∈
𝐵 𝐹 = {〈𝑧, 𝑦〉} → 𝐹 ∈ V) |
16 | | eleq1 2233 |
. . . 4
⊢ (𝑤 = 𝐹 → (𝑤 ∈ X𝑥 ∈ {𝑧}𝐵 ↔ 𝐹 ∈ X𝑥 ∈ {𝑧}𝐵)) |
17 | | eqeq1 2177 |
. . . . 5
⊢ (𝑤 = 𝐹 → (𝑤 = {〈𝑧, 𝑦〉} ↔ 𝐹 = {〈𝑧, 𝑦〉})) |
18 | 17 | rexbidv 2471 |
. . . 4
⊢ (𝑤 = 𝐹 → (∃𝑦 ∈ 𝐵 𝑤 = {〈𝑧, 𝑦〉} ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝑧, 𝑦〉})) |
19 | | vex 2733 |
. . . . . 6
⊢ 𝑤 ∈ V |
20 | 19 | elixp 6679 |
. . . . 5
⊢ (𝑤 ∈ X𝑥 ∈
{𝑧}𝐵 ↔ (𝑤 Fn {𝑧} ∧ ∀𝑥 ∈ {𝑧} (𝑤‘𝑥) ∈ 𝐵)) |
21 | | fveq2 5494 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → (𝑤‘𝑥) = (𝑤‘𝑧)) |
22 | 21 | eleq1d 2239 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → ((𝑤‘𝑥) ∈ 𝐵 ↔ (𝑤‘𝑧) ∈ 𝐵)) |
23 | 9, 22 | ralsn 3624 |
. . . . . 6
⊢
(∀𝑥 ∈
{𝑧} (𝑤‘𝑥) ∈ 𝐵 ↔ (𝑤‘𝑧) ∈ 𝐵) |
24 | 23 | anbi2i 454 |
. . . . 5
⊢ ((𝑤 Fn {𝑧} ∧ ∀𝑥 ∈ {𝑧} (𝑤‘𝑥) ∈ 𝐵) ↔ (𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵)) |
25 | | simpl 108 |
. . . . . . . . 9
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) → 𝑤 Fn {𝑧}) |
26 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑤‘𝑦) = (𝑤‘𝑧)) |
27 | 26 | eleq1d 2239 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → ((𝑤‘𝑦) ∈ 𝐵 ↔ (𝑤‘𝑧) ∈ 𝐵)) |
28 | 9, 27 | ralsn 3624 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
{𝑧} (𝑤‘𝑦) ∈ 𝐵 ↔ (𝑤‘𝑧) ∈ 𝐵) |
29 | 28 | biimpri 132 |
. . . . . . . . . 10
⊢ ((𝑤‘𝑧) ∈ 𝐵 → ∀𝑦 ∈ {𝑧} (𝑤‘𝑦) ∈ 𝐵) |
30 | 29 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) → ∀𝑦 ∈ {𝑧} (𝑤‘𝑦) ∈ 𝐵) |
31 | | ffnfv 5651 |
. . . . . . . . 9
⊢ (𝑤:{𝑧}⟶𝐵 ↔ (𝑤 Fn {𝑧} ∧ ∀𝑦 ∈ {𝑧} (𝑤‘𝑦) ∈ 𝐵)) |
32 | 25, 30, 31 | sylanbrc 415 |
. . . . . . . 8
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) → 𝑤:{𝑧}⟶𝐵) |
33 | 9 | fsn2 5667 |
. . . . . . . 8
⊢ (𝑤:{𝑧}⟶𝐵 ↔ ((𝑤‘𝑧) ∈ 𝐵 ∧ 𝑤 = {〈𝑧, (𝑤‘𝑧)〉})) |
34 | 32, 33 | sylib 121 |
. . . . . . 7
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) → ((𝑤‘𝑧) ∈ 𝐵 ∧ 𝑤 = {〈𝑧, (𝑤‘𝑧)〉})) |
35 | | opeq2 3764 |
. . . . . . . . 9
⊢ (𝑦 = (𝑤‘𝑧) → 〈𝑧, 𝑦〉 = 〈𝑧, (𝑤‘𝑧)〉) |
36 | 35 | sneqd 3594 |
. . . . . . . 8
⊢ (𝑦 = (𝑤‘𝑧) → {〈𝑧, 𝑦〉} = {〈𝑧, (𝑤‘𝑧)〉}) |
37 | 36 | rspceeqv 2852 |
. . . . . . 7
⊢ (((𝑤‘𝑧) ∈ 𝐵 ∧ 𝑤 = {〈𝑧, (𝑤‘𝑧)〉}) → ∃𝑦 ∈ 𝐵 𝑤 = {〈𝑧, 𝑦〉}) |
38 | 34, 37 | syl 14 |
. . . . . 6
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) → ∃𝑦 ∈ 𝐵 𝑤 = {〈𝑧, 𝑦〉}) |
39 | 9, 10 | fvsn 5688 |
. . . . . . . . . 10
⊢
({〈𝑧, 𝑦〉}‘𝑧) = 𝑦 |
40 | | id 19 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵) |
41 | 39, 40 | eqeltrid 2257 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ({〈𝑧, 𝑦〉}‘𝑧) ∈ 𝐵) |
42 | 9, 10 | fnsn 5250 |
. . . . . . . . 9
⊢
{〈𝑧, 𝑦〉} Fn {𝑧} |
43 | 41, 42 | jctil 310 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → ({〈𝑧, 𝑦〉} Fn {𝑧} ∧ ({〈𝑧, 𝑦〉}‘𝑧) ∈ 𝐵)) |
44 | | fneq1 5284 |
. . . . . . . . 9
⊢ (𝑤 = {〈𝑧, 𝑦〉} → (𝑤 Fn {𝑧} ↔ {〈𝑧, 𝑦〉} Fn {𝑧})) |
45 | | fveq1 5493 |
. . . . . . . . . 10
⊢ (𝑤 = {〈𝑧, 𝑦〉} → (𝑤‘𝑧) = ({〈𝑧, 𝑦〉}‘𝑧)) |
46 | 45 | eleq1d 2239 |
. . . . . . . . 9
⊢ (𝑤 = {〈𝑧, 𝑦〉} → ((𝑤‘𝑧) ∈ 𝐵 ↔ ({〈𝑧, 𝑦〉}‘𝑧) ∈ 𝐵)) |
47 | 44, 46 | anbi12d 470 |
. . . . . . . 8
⊢ (𝑤 = {〈𝑧, 𝑦〉} → ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) ↔ ({〈𝑧, 𝑦〉} Fn {𝑧} ∧ ({〈𝑧, 𝑦〉}‘𝑧) ∈ 𝐵))) |
48 | 43, 47 | syl5ibrcom 156 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐵 → (𝑤 = {〈𝑧, 𝑦〉} → (𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵))) |
49 | 48 | rexlimiv 2581 |
. . . . . 6
⊢
(∃𝑦 ∈
𝐵 𝑤 = {〈𝑧, 𝑦〉} → (𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵)) |
50 | 38, 49 | impbii 125 |
. . . . 5
⊢ ((𝑤 Fn {𝑧} ∧ (𝑤‘𝑧) ∈ 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑤 = {〈𝑧, 𝑦〉}) |
51 | 20, 24, 50 | 3bitri 205 |
. . . 4
⊢ (𝑤 ∈ X𝑥 ∈
{𝑧}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝑤 = {〈𝑧, 𝑦〉}) |
52 | 16, 18, 51 | vtoclbg 2791 |
. . 3
⊢ (𝐹 ∈ V → (𝐹 ∈ X𝑥 ∈
{𝑧}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝑧, 𝑦〉})) |
53 | 8, 15, 52 | pm5.21nii 699 |
. 2
⊢ (𝐹 ∈ X𝑥 ∈
{𝑧}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝑧, 𝑦〉}) |
54 | 3, 7, 53 | vtoclbg 2791 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ X𝑥 ∈ {𝐴}𝐵 ↔ ∃𝑦 ∈ 𝐵 𝐹 = {〈𝐴, 𝑦〉})) |