Step |
Hyp |
Ref |
Expression |
1 |
|
xpsnen.1 |
⊢ 𝐴 ∈ V |
2 |
|
xpsnen.2 |
⊢ 𝐵 ∈ V |
3 |
|
snex |
⊢ { 𝐵 } ∈ V |
4 |
1 3
|
xpex |
⊢ ( 𝐴 × { 𝐵 } ) ∈ V |
5 |
|
elxp |
⊢ ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ∃ 𝑥 ∃ 𝑧 ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ) |
6 |
|
inteq |
⊢ ( 𝑦 = 〈 𝑥 , 𝑧 〉 → ∩ 𝑦 = ∩ 〈 𝑥 , 𝑧 〉 ) |
7 |
6
|
inteqd |
⊢ ( 𝑦 = 〈 𝑥 , 𝑧 〉 → ∩ ∩ 𝑦 = ∩ ∩ 〈 𝑥 , 𝑧 〉 ) |
8 |
|
vex |
⊢ 𝑥 ∈ V |
9 |
|
vex |
⊢ 𝑧 ∈ V |
10 |
8 9
|
op1stb |
⊢ ∩ ∩ 〈 𝑥 , 𝑧 〉 = 𝑥 |
11 |
7 10
|
eqtrdi |
⊢ ( 𝑦 = 〈 𝑥 , 𝑧 〉 → ∩ ∩ 𝑦 = 𝑥 ) |
12 |
11 8
|
eqeltrdi |
⊢ ( 𝑦 = 〈 𝑥 , 𝑧 〉 → ∩ ∩ 𝑦 ∈ V ) |
13 |
12
|
adantr |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) → ∩ ∩ 𝑦 ∈ V ) |
14 |
13
|
exlimivv |
⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) → ∩ ∩ 𝑦 ∈ V ) |
15 |
5 14
|
sylbi |
⊢ ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) → ∩ ∩ 𝑦 ∈ V ) |
16 |
|
opex |
⊢ 〈 𝑥 , 𝐵 〉 ∈ V |
17 |
16
|
a1i |
⊢ ( 𝑥 ∈ 𝐴 → 〈 𝑥 , 𝐵 〉 ∈ V ) |
18 |
|
eqvisset |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → ∩ ∩ 𝑦 ∈ V ) |
19 |
|
ancom |
⊢ ( ( ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑧 ∈ { 𝐵 } ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
20 |
|
anass |
⊢ ( ( ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ { 𝐵 } ) ↔ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ) |
21 |
|
velsn |
⊢ ( 𝑧 ∈ { 𝐵 } ↔ 𝑧 = 𝐵 ) |
22 |
21
|
anbi1i |
⊢ ( ( 𝑧 ∈ { 𝐵 } ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ↔ ( 𝑧 = 𝐵 ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
23 |
19 20 22
|
3bitr3i |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ↔ ( 𝑧 = 𝐵 ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
24 |
23
|
exbii |
⊢ ( ∃ 𝑧 ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝐵 ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
25 |
|
opeq2 |
⊢ ( 𝑧 = 𝐵 → 〈 𝑥 , 𝑧 〉 = 〈 𝑥 , 𝐵 〉 ) |
26 |
25
|
eqeq2d |
⊢ ( 𝑧 = 𝐵 → ( 𝑦 = 〈 𝑥 , 𝑧 〉 ↔ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ) |
27 |
26
|
anbi1d |
⊢ ( 𝑧 = 𝐵 → ( ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
28 |
2 27
|
ceqsexv |
⊢ ( ∃ 𝑧 ( 𝑧 = 𝐵 ∧ ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ 𝑥 ∈ 𝐴 ) ) ↔ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) |
29 |
|
inteq |
⊢ ( 𝑦 = 〈 𝑥 , 𝐵 〉 → ∩ 𝑦 = ∩ 〈 𝑥 , 𝐵 〉 ) |
30 |
29
|
inteqd |
⊢ ( 𝑦 = 〈 𝑥 , 𝐵 〉 → ∩ ∩ 𝑦 = ∩ ∩ 〈 𝑥 , 𝐵 〉 ) |
31 |
8 2
|
op1stb |
⊢ ∩ ∩ 〈 𝑥 , 𝐵 〉 = 𝑥 |
32 |
30 31
|
eqtr2di |
⊢ ( 𝑦 = 〈 𝑥 , 𝐵 〉 → 𝑥 = ∩ ∩ 𝑦 ) |
33 |
32
|
pm4.71ri |
⊢ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ↔ ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ) |
34 |
33
|
anbi1i |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ∧ 𝑥 ∈ 𝐴 ) ) |
35 |
|
anass |
⊢ ( ( ( 𝑥 = ∩ ∩ 𝑦 ∧ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
36 |
34 35
|
bitri |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
37 |
24 28 36
|
3bitri |
⊢ ( ∃ 𝑧 ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ↔ ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
38 |
37
|
exbii |
⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑦 = 〈 𝑥 , 𝑧 〉 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ { 𝐵 } ) ) ↔ ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
39 |
5 38
|
bitri |
⊢ ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ) |
40 |
|
opeq1 |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → 〈 𝑥 , 𝐵 〉 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ) |
41 |
40
|
eqeq2d |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑦 = 〈 𝑥 , 𝐵 〉 ↔ 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ) ) |
42 |
|
eleq1 |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑥 ∈ 𝐴 ↔ ∩ ∩ 𝑦 ∈ 𝐴 ) ) |
43 |
41 42
|
anbi12d |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ) ) |
44 |
43
|
ceqsexgv |
⊢ ( ∩ ∩ 𝑦 ∈ V → ( ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝑦 ∧ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) ↔ ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ) ) |
45 |
39 44
|
syl5bb |
⊢ ( ∩ ∩ 𝑦 ∈ V → ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ) ) |
46 |
18 45
|
syl |
⊢ ( 𝑥 = ∩ ∩ 𝑦 → ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ↔ ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ) ) |
47 |
46
|
pm5.32ri |
⊢ ( ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ↔ ( ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ) |
48 |
32
|
adantr |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 = ∩ ∩ 𝑦 ) |
49 |
48
|
pm4.71i |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ) |
50 |
43
|
pm5.32ri |
⊢ ( ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ↔ ( ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ) |
51 |
49 50
|
bitr2i |
⊢ ( ( ( 𝑦 = 〈 ∩ ∩ 𝑦 , 𝐵 〉 ∧ ∩ ∩ 𝑦 ∈ 𝐴 ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ↔ ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ) |
52 |
|
ancom |
⊢ ( ( 𝑦 = 〈 𝑥 , 𝐵 〉 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ) |
53 |
47 51 52
|
3bitri |
⊢ ( ( 𝑦 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 = ∩ ∩ 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 〈 𝑥 , 𝐵 〉 ) ) |
54 |
4 1 15 17 53
|
en2i |
⊢ ( 𝐴 × { 𝐵 } ) ≈ 𝐴 |