Step |
Hyp |
Ref |
Expression |
1 |
|
elxp7 |
⊢ ( 𝑤 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) |
2 |
1
|
anbi2i |
⊢ ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
3 |
|
anass |
⊢ ( ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
4 |
3
|
a1i |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) ) |
5 |
|
ssel |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( 1st ‘ 𝑤 ) ∈ 𝐴 → ( 1st ‘ 𝑤 ) ∈ 𝐵 ) ) |
6 |
5
|
pm4.71d |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1st ‘ 𝑤 ) ∈ 𝐵 ) ) ) |
7 |
6
|
anbi1d |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 1st ‘ 𝑤 ) ∈ 𝐵 ) ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
8 |
|
an12 |
⊢ ( ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) |
9 |
8
|
anbi2i |
⊢ ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
10 |
9
|
a1i |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) ) |
11 |
4 7 10
|
3bitr4d |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐵 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) ) |
12 |
2 11
|
bitr4id |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
13 |
|
an12 |
⊢ ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 𝑤 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) |
14 |
12 13
|
bitrdi |
⊢ ( 𝐴 ⊆ 𝐵 → ( ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) ) |
15 |
|
cnvresima |
⊢ ( ◡ ( 1st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( ( ◡ 1st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) ) |
16 |
15
|
eleq2i |
⊢ ( 𝑤 ∈ ( ◡ ( 1st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ 𝑤 ∈ ( ( ◡ 1st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) ) ) |
17 |
|
elin |
⊢ ( 𝑤 ∈ ( ( ◡ 1st “ 𝐴 ) ∩ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑤 ∈ ( ◡ 1st “ 𝐴 ) ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ) |
18 |
|
vex |
⊢ 𝑤 ∈ V |
19 |
|
fo1st |
⊢ 1st : V –onto→ V |
20 |
|
fofn |
⊢ ( 1st : V –onto→ V → 1st Fn V ) |
21 |
|
elpreima |
⊢ ( 1st Fn V → ( 𝑤 ∈ ( ◡ 1st “ 𝐴 ) ↔ ( 𝑤 ∈ V ∧ ( 1st ‘ 𝑤 ) ∈ 𝐴 ) ) ) |
22 |
19 20 21
|
mp2b |
⊢ ( 𝑤 ∈ ( ◡ 1st “ 𝐴 ) ↔ ( 𝑤 ∈ V ∧ ( 1st ‘ 𝑤 ) ∈ 𝐴 ) ) |
23 |
18 22
|
mpbiran |
⊢ ( 𝑤 ∈ ( ◡ 1st “ 𝐴 ) ↔ ( 1st ‘ 𝑤 ) ∈ 𝐴 ) |
24 |
23
|
anbi1i |
⊢ ( ( 𝑤 ∈ ( ◡ 1st “ 𝐴 ) ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ) |
25 |
16 17 24
|
3bitri |
⊢ ( 𝑤 ∈ ( ◡ ( 1st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ 𝑤 ∈ ( 𝐵 × 𝐶 ) ) ) |
26 |
|
elxp7 |
⊢ ( 𝑤 ∈ ( 𝐴 × 𝐶 ) ↔ ( 𝑤 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑤 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑤 ) ∈ 𝐶 ) ) ) |
27 |
14 25 26
|
3bitr4g |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑤 ∈ ( ◡ ( 1st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) ↔ 𝑤 ∈ ( 𝐴 × 𝐶 ) ) ) |
28 |
27
|
eqrdv |
⊢ ( 𝐴 ⊆ 𝐵 → ( ◡ ( 1st ↾ ( 𝐵 × 𝐶 ) ) “ 𝐴 ) = ( 𝐴 × 𝐶 ) ) |