Step |
Hyp |
Ref |
Expression |
1 |
|
bropfvvvv.o |
⊢ 𝑂 = ( 𝑎 ∈ 𝑈 ↦ ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜑 } ) ) |
2 |
|
bropfvvvv.oo |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) → ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) = { 〈 𝑑 , 𝑒 〉 ∣ 𝜃 } ) |
3 |
|
bropfvvvv.s |
⊢ ( 𝑎 = 𝐴 → 𝑉 = 𝑆 ) |
4 |
|
bropfvvvv.t |
⊢ ( 𝑎 = 𝐴 → 𝑊 = 𝑇 ) |
5 |
|
bropfvvvv.p |
⊢ ( 𝑎 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) |
6 |
|
brovpreldm |
⊢ ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) ) |
7 |
5
|
opabbidv |
⊢ ( 𝑎 = 𝐴 → { 〈 𝑑 , 𝑒 〉 ∣ 𝜑 } = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) |
8 |
3 4 7
|
mpoeq123dv |
⊢ ( 𝑎 = 𝐴 → ( 𝑏 ∈ 𝑉 , 𝑐 ∈ 𝑊 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜑 } ) = ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ) |
9 |
8 1
|
fvmptg |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( 𝑂 ‘ 𝐴 ) = ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ) |
10 |
9
|
dmeqd |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → dom ( 𝑂 ‘ 𝐴 ) = dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ) |
11 |
10
|
eleq2d |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ) ) |
12 |
|
dmoprabss |
⊢ dom { 〈 〈 𝑏 , 𝑐 〉 , 𝑧 〉 ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) } ⊆ ( 𝑆 × 𝑇 ) |
13 |
12
|
sseli |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ dom { 〈 〈 𝑏 , 𝑐 〉 , 𝑧 〉 ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) } → 〈 𝐵 , 𝐶 〉 ∈ ( 𝑆 × 𝑇 ) ) |
14 |
1 2
|
bropfvvvvlem |
⊢ ( ( 〈 𝐵 , 𝐶 〉 ∈ ( 𝑆 × 𝑇 ) ∧ 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) |
15 |
14
|
ex |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ ( 𝑆 × 𝑇 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) |
16 |
13 15
|
syl |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ dom { 〈 〈 𝑏 , 𝑐 〉 , 𝑧 〉 ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) } → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) |
17 |
|
df-mpo |
⊢ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) = { 〈 〈 𝑏 , 𝑐 〉 , 𝑧 〉 ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) } |
18 |
17
|
dmeqi |
⊢ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) = dom { 〈 〈 𝑏 , 𝑐 〉 , 𝑧 〉 ∣ ( ( 𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇 ) ∧ 𝑧 = { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) } |
19 |
16 18
|
eleq2s |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) |
20 |
11 19
|
syl6bi |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) |
21 |
20
|
com23 |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) |
22 |
21
|
a1d |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
23 |
|
ianor |
⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) ↔ ( ¬ 𝐴 ∈ 𝑈 ∨ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) ) |
24 |
1
|
fvmptndm |
⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 𝑂 ‘ 𝐴 ) = ∅ ) |
25 |
24
|
dmeqd |
⊢ ( ¬ 𝐴 ∈ 𝑈 → dom ( 𝑂 ‘ 𝐴 ) = dom ∅ ) |
26 |
25
|
eleq2d |
⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ 〈 𝐵 , 𝐶 〉 ∈ dom ∅ ) ) |
27 |
|
dm0 |
⊢ dom ∅ = ∅ |
28 |
27
|
eleq2i |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ dom ∅ ↔ 〈 𝐵 , 𝐶 〉 ∈ ∅ ) |
29 |
26 28
|
bitrdi |
⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) ↔ 〈 𝐵 , 𝐶 〉 ∈ ∅ ) ) |
30 |
|
noel |
⊢ ¬ 〈 𝐵 , 𝐶 〉 ∈ ∅ |
31 |
30
|
pm2.21i |
⊢ ( 〈 𝐵 , 𝐶 〉 ∈ ∅ → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) |
32 |
29 31
|
syl6bi |
⊢ ( ¬ 𝐴 ∈ 𝑈 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) |
33 |
32
|
a1d |
⊢ ( ¬ 𝐴 ∈ 𝑈 → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
34 |
|
notnotb |
⊢ ( 𝐴 ∈ 𝑈 ↔ ¬ ¬ 𝐴 ∈ 𝑈 ) |
35 |
|
elex |
⊢ ( 𝑆 ∈ 𝑋 → 𝑆 ∈ V ) |
36 |
|
elex |
⊢ ( 𝑇 ∈ 𝑌 → 𝑇 ∈ V ) |
37 |
35 36
|
anim12i |
⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) |
38 |
37
|
adantl |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) |
39 |
|
mpoexga |
⊢ ( ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) |
40 |
38 39
|
syl |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) |
41 |
40
|
pm2.24d |
⊢ ( ( 𝐴 ∈ 𝑈 ∧ ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) ) → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
42 |
41
|
ex |
⊢ ( 𝐴 ∈ 𝑈 → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) ) |
43 |
42
|
com23 |
⊢ ( 𝐴 ∈ 𝑈 → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) ) |
44 |
34 43
|
sylbir |
⊢ ( ¬ ¬ 𝐴 ∈ 𝑈 → ( ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) ) |
45 |
44
|
imp |
⊢ ( ( ¬ ¬ 𝐴 ∈ 𝑈 ∧ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
46 |
33 45
|
jaoi3 |
⊢ ( ( ¬ 𝐴 ∈ 𝑈 ∨ ¬ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
47 |
23 46
|
sylbi |
⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
48 |
47
|
com34 |
⊢ ( ¬ ( 𝐴 ∈ 𝑈 ∧ ( 𝑏 ∈ 𝑆 , 𝑐 ∈ 𝑇 ↦ { 〈 𝑑 , 𝑒 〉 ∣ 𝜓 } ) ∈ V ) → ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) ) |
49 |
22 48
|
pm2.61i |
⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 〈 𝐵 , 𝐶 〉 ∈ dom ( 𝑂 ‘ 𝐴 ) → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) ) |
50 |
6 49
|
mpdi |
⊢ ( ( 𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌 ) → ( 𝐷 ( 𝐵 ( 𝑂 ‘ 𝐴 ) 𝐶 ) 𝐸 → ( 𝐴 ∈ 𝑈 ∧ ( 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇 ) ∧ ( 𝐷 ∈ V ∧ 𝐸 ∈ V ) ) ) ) |