Step |
Hyp |
Ref |
Expression |
1 |
|
funfn |
⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 ) |
2 |
|
fncnvima2 |
⊢ ( 𝐹 Fn dom 𝐹 → ( ◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } ) |
3 |
1 2
|
sylbi |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } ) |
4 |
3
|
adantr |
⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } ) |
5 |
|
elxp6 |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) 〉 ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) ) |
6 |
|
fvco |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) = ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
7 |
|
fvco |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) = ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ) |
8 |
6 7
|
opeq12d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) 〉 ) |
9 |
8
|
eqeq2d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ↔ ( 𝐹 ‘ 𝑥 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) 〉 ) ) |
10 |
6
|
eleq1d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ) ) |
11 |
7
|
eleq1d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) |
12 |
10 11
|
anbi12d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) ) |
13 |
9 12
|
anbi12d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ∧ ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 〈 ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) 〉 ∧ ( ( 1st ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑌 ∧ ( 2nd ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝑍 ) ) ) ) |
14 |
5 13
|
bitr4id |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ∧ ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) ) |
15 |
14
|
adantlr |
⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ∧ ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) ) |
16 |
|
opfv |
⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ) |
17 |
16
|
biantrurd |
⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = 〈 ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) , ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) 〉 ∧ ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ) ) ) |
18 |
|
fo1st |
⊢ 1st : V –onto→ V |
19 |
|
fofun |
⊢ ( 1st : V –onto→ V → Fun 1st ) |
20 |
18 19
|
ax-mp |
⊢ Fun 1st |
21 |
|
funco |
⊢ ( ( Fun 1st ∧ Fun 𝐹 ) → Fun ( 1st ∘ 𝐹 ) ) |
22 |
20 21
|
mpan |
⊢ ( Fun 𝐹 → Fun ( 1st ∘ 𝐹 ) ) |
23 |
22
|
adantr |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → Fun ( 1st ∘ 𝐹 ) ) |
24 |
|
ssv |
⊢ ( 𝐹 “ dom 𝐹 ) ⊆ V |
25 |
|
fof |
⊢ ( 1st : V –onto→ V → 1st : V ⟶ V ) |
26 |
|
fdm |
⊢ ( 1st : V ⟶ V → dom 1st = V ) |
27 |
18 25 26
|
mp2b |
⊢ dom 1st = V |
28 |
24 27
|
sseqtrri |
⊢ ( 𝐹 “ dom 𝐹 ) ⊆ dom 1st |
29 |
|
ssid |
⊢ dom 𝐹 ⊆ dom 𝐹 |
30 |
|
funimass3 |
⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹 ) → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 1st ↔ dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 1st ) ) ) |
31 |
29 30
|
mpan2 |
⊢ ( Fun 𝐹 → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 1st ↔ dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 1st ) ) ) |
32 |
28 31
|
mpbii |
⊢ ( Fun 𝐹 → dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 1st ) ) |
33 |
32
|
sselda |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ◡ 𝐹 “ dom 1st ) ) |
34 |
|
dmco |
⊢ dom ( 1st ∘ 𝐹 ) = ( ◡ 𝐹 “ dom 1st ) |
35 |
33 34
|
eleqtrrdi |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ dom ( 1st ∘ 𝐹 ) ) |
36 |
|
fvimacnv |
⊢ ( ( Fun ( 1st ∘ 𝐹 ) ∧ 𝑥 ∈ dom ( 1st ∘ 𝐹 ) ) → ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) ) |
37 |
23 35 36
|
syl2anc |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ↔ 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) ) |
38 |
|
fo2nd |
⊢ 2nd : V –onto→ V |
39 |
|
fofun |
⊢ ( 2nd : V –onto→ V → Fun 2nd ) |
40 |
38 39
|
ax-mp |
⊢ Fun 2nd |
41 |
|
funco |
⊢ ( ( Fun 2nd ∧ Fun 𝐹 ) → Fun ( 2nd ∘ 𝐹 ) ) |
42 |
40 41
|
mpan |
⊢ ( Fun 𝐹 → Fun ( 2nd ∘ 𝐹 ) ) |
43 |
42
|
adantr |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → Fun ( 2nd ∘ 𝐹 ) ) |
44 |
|
fof |
⊢ ( 2nd : V –onto→ V → 2nd : V ⟶ V ) |
45 |
|
fdm |
⊢ ( 2nd : V ⟶ V → dom 2nd = V ) |
46 |
38 44 45
|
mp2b |
⊢ dom 2nd = V |
47 |
24 46
|
sseqtrri |
⊢ ( 𝐹 “ dom 𝐹 ) ⊆ dom 2nd |
48 |
|
funimass3 |
⊢ ( ( Fun 𝐹 ∧ dom 𝐹 ⊆ dom 𝐹 ) → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 2nd ↔ dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 2nd ) ) ) |
49 |
29 48
|
mpan2 |
⊢ ( Fun 𝐹 → ( ( 𝐹 “ dom 𝐹 ) ⊆ dom 2nd ↔ dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 2nd ) ) ) |
50 |
47 49
|
mpbii |
⊢ ( Fun 𝐹 → dom 𝐹 ⊆ ( ◡ 𝐹 “ dom 2nd ) ) |
51 |
50
|
sselda |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ◡ 𝐹 “ dom 2nd ) ) |
52 |
|
dmco |
⊢ dom ( 2nd ∘ 𝐹 ) = ( ◡ 𝐹 “ dom 2nd ) |
53 |
51 52
|
eleqtrrdi |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ dom ( 2nd ∘ 𝐹 ) ) |
54 |
|
fvimacnv |
⊢ ( ( Fun ( 2nd ∘ 𝐹 ) ∧ 𝑥 ∈ dom ( 2nd ∘ 𝐹 ) ) → ( ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) |
55 |
43 53 54
|
syl2anc |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ↔ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) |
56 |
37 55
|
anbi12d |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) ) |
57 |
56
|
adantlr |
⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( ( ( 1st ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑌 ∧ ( ( 2nd ∘ 𝐹 ) ‘ 𝑥 ) ∈ 𝑍 ) ↔ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) ) |
58 |
15 17 57
|
3bitr2d |
⊢ ( ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) ↔ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) ) |
59 |
58
|
rabbidva |
⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → { 𝑥 ∈ dom 𝐹 ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑌 × 𝑍 ) } = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) } ) |
60 |
4 59
|
eqtrd |
⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) } ) |
61 |
|
dfin5 |
⊢ ( dom 𝐹 ∩ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) = { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) } |
62 |
|
dfin5 |
⊢ ( dom 𝐹 ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) = { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) } |
63 |
61 62
|
ineq12i |
⊢ ( ( dom 𝐹 ∩ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) ∩ ( dom 𝐹 ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) = ( { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) } ∩ { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) } ) |
64 |
|
cnvimass |
⊢ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom ( 1st ∘ 𝐹 ) |
65 |
|
dmcoss |
⊢ dom ( 1st ∘ 𝐹 ) ⊆ dom 𝐹 |
66 |
64 65
|
sstri |
⊢ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom 𝐹 |
67 |
|
sseqin2 |
⊢ ( ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) = ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) |
68 |
66 67
|
mpbi |
⊢ ( dom 𝐹 ∩ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) = ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) |
69 |
|
cnvimass |
⊢ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom ( 2nd ∘ 𝐹 ) |
70 |
|
dmcoss |
⊢ dom ( 2nd ∘ 𝐹 ) ⊆ dom 𝐹 |
71 |
69 70
|
sstri |
⊢ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom 𝐹 |
72 |
|
sseqin2 |
⊢ ( ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ⊆ dom 𝐹 ↔ ( dom 𝐹 ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) = ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) |
73 |
71 72
|
mpbi |
⊢ ( dom 𝐹 ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) = ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) |
74 |
68 73
|
ineq12i |
⊢ ( ( dom 𝐹 ∩ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ) ∩ ( dom 𝐹 ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) = ( ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) |
75 |
|
inrab |
⊢ ( { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) } ∩ { 𝑥 ∈ dom 𝐹 ∣ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) } ) = { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) } |
76 |
63 74 75
|
3eqtr3ri |
⊢ { 𝑥 ∈ dom 𝐹 ∣ ( 𝑥 ∈ ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∧ 𝑥 ∈ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) } = ( ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) |
77 |
60 76
|
eqtrdi |
⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( V × V ) ) → ( ◡ 𝐹 “ ( 𝑌 × 𝑍 ) ) = ( ( ◡ ( 1st ∘ 𝐹 ) “ 𝑌 ) ∩ ( ◡ ( 2nd ∘ 𝐹 ) “ 𝑍 ) ) ) |