Step | Hyp | Ref
| Expression |
1 | | elex 3447 |
. 2
⊢ (𝐴 ∈ (𝑅 “ 𝐵) → 𝐴 ∈ V) |
2 | | xpeq2 5605 |
. . . . . . 7
⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = (𝐵 × ∅)) |
3 | | xp0 6054 |
. . . . . . 7
⊢ (𝐵 × ∅) =
∅ |
4 | 2, 3 | eqtrdi 2794 |
. . . . . 6
⊢ ({𝐴} = ∅ → (𝐵 × {𝐴}) = ∅) |
5 | 4 | ineq2d 4146 |
. . . . 5
⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = (𝑅 ∩ ∅)) |
6 | | in0 4325 |
. . . . 5
⊢ (𝑅 ∩ ∅) =
∅ |
7 | 5, 6 | eqtrdi 2794 |
. . . 4
⊢ ({𝐴} = ∅ → (𝑅 ∩ (𝐵 × {𝐴})) = ∅) |
8 | 7 | necon3i 2976 |
. . 3
⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → {𝐴} ≠ ∅) |
9 | | snnzb 4654 |
. . 3
⊢ (𝐴 ∈ V ↔ {𝐴} ≠ ∅) |
10 | 8, 9 | sylibr 233 |
. 2
⊢ ((𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅ → 𝐴 ∈ V) |
11 | | eleq1 2826 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑥 ∈ (𝑅 “ 𝐵) ↔ 𝐴 ∈ (𝑅 “ 𝐵))) |
12 | | sneq 4571 |
. . . . . 6
⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴}) |
13 | 12 | xpeq2d 5614 |
. . . . 5
⊢ (𝑥 = 𝐴 → (𝐵 × {𝑥}) = (𝐵 × {𝐴})) |
14 | 13 | ineq2d 4146 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑅 ∩ (𝐵 × {𝑥})) = (𝑅 ∩ (𝐵 × {𝐴}))) |
15 | 14 | neeq1d 3003 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)) |
16 | | elin 3902 |
. . . . . . 7
⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥}))) |
17 | | ancom 461 |
. . . . . . 7
⊢ ((𝑝 ∈ 𝑅 ∧ 𝑝 ∈ (𝐵 × {𝑥})) ↔ (𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅)) |
18 | | elxp 5607 |
. . . . . . . 8
⊢ (𝑝 ∈ (𝐵 × {𝑥}) ↔ ∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}))) |
19 | 18 | anbi1i 624 |
. . . . . . 7
⊢ ((𝑝 ∈ (𝐵 × {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
20 | 16, 17, 19 | 3bitri 297 |
. . . . . 6
⊢ (𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ (∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
21 | 20 | exbii 1850 |
. . . . 5
⊢
(∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
22 | | anass 469 |
. . . . . . . . 9
⊢ (((𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅))) |
23 | 22 | 2exbii 1851 |
. . . . . . . 8
⊢
(∃𝑦∃𝑧((𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅))) |
24 | | 19.41vv 1954 |
. . . . . . . 8
⊢
(∃𝑦∃𝑧((𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ (∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
25 | 23, 24 | bitr3i 276 |
. . . . . . 7
⊢
(∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
26 | 25 | exbii 1850 |
. . . . . 6
⊢
(∃𝑝∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑝(∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅)) |
27 | | exrot3 2165 |
. . . . . 6
⊢
(∃𝑝∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅))) |
28 | 26, 27 | bitr3i 276 |
. . . . 5
⊢
(∃𝑝(∃𝑦∃𝑧(𝑝 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥})) ∧ 𝑝 ∈ 𝑅) ↔ ∃𝑦∃𝑧∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅))) |
29 | | opex 5377 |
. . . . . . . . 9
⊢
〈𝑦, 𝑧〉 ∈ V |
30 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑦, 𝑧〉 → (𝑝 ∈ 𝑅 ↔ 〈𝑦, 𝑧〉 ∈ 𝑅)) |
31 | 30 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝑦, 𝑧〉 → (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
32 | 29, 31 | ceqsexv 3476 |
. . . . . . . 8
⊢
(∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅)) |
33 | 32 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑧∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅)) |
34 | | anass 469 |
. . . . . . . . 9
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
35 | | an12 642 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ∧ (𝑧 ∈ {𝑥} ∧ 〈𝑦, 𝑧〉 ∈ 𝑅)) ↔ (𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
36 | | velsn 4577 |
. . . . . . . . . 10
⊢ (𝑧 ∈ {𝑥} ↔ 𝑧 = 𝑥) |
37 | 36 | anbi1i 624 |
. . . . . . . . 9
⊢ ((𝑧 ∈ {𝑥} ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅)) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
38 | 34, 35, 37 | 3bitri 297 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅) ↔ (𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
39 | 38 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑧((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 〈𝑦, 𝑧〉 ∈ 𝑅) ↔ ∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅))) |
40 | | vex 3433 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
41 | | opeq2 4805 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → 〈𝑦, 𝑧〉 = 〈𝑦, 𝑥〉) |
42 | 41 | eleq1d 2823 |
. . . . . . . . 9
⊢ (𝑧 = 𝑥 → (〈𝑦, 𝑧〉 ∈ 𝑅 ↔ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
43 | 42 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → ((𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅) ↔ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅))) |
44 | 40, 43 | ceqsexv 3476 |
. . . . . . 7
⊢
(∃𝑧(𝑧 = 𝑥 ∧ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑧〉 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
45 | 33, 39, 44 | 3bitri 297 |
. . . . . 6
⊢
(∃𝑧∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ (𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
46 | 45 | exbii 1850 |
. . . . 5
⊢
(∃𝑦∃𝑧∃𝑝(𝑝 = 〈𝑦, 𝑧〉 ∧ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ {𝑥}) ∧ 𝑝 ∈ 𝑅)) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
47 | 21, 28, 46 | 3bitri 297 |
. . . 4
⊢
(∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥})) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
48 | | n0 4280 |
. . . 4
⊢ ((𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (𝑅 ∩ (𝐵 × {𝑥}))) |
49 | 40 | elima3 5969 |
. . . 4
⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ ∃𝑦(𝑦 ∈ 𝐵 ∧ 〈𝑦, 𝑥〉 ∈ 𝑅)) |
50 | 47, 48, 49 | 3bitr4ri 304 |
. . 3
⊢ (𝑥 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝑥})) ≠ ∅) |
51 | 11, 15, 50 | vtoclbg 3504 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅)) |
52 | 1, 10, 51 | pm5.21nii 380 |
1
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅) |