Step | Hyp | Ref
| Expression |
1 | | brovpreldm 7141 |
. 2
⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → 〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴)) |
2 | | bropfvvvv.o |
. . . . . . . . . 10
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) |
3 | 2 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑}))) |
4 | | bropfvvvv.s |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → 𝑉 = 𝑆) |
5 | | bropfvvvv.t |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → 𝑊 = 𝑇) |
6 | | bropfvvvv.p |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) |
7 | 6 | opabbidv 4648 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → {〈𝑑, 𝑒〉 ∣ 𝜑} = {〈𝑑, 𝑒〉 ∣ 𝜓}) |
8 | 4, 5, 7 | mpt2eq123dv 6615 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑}) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓})) |
9 | 8 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) ∧ 𝑎 = 𝐴) → (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑}) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓})) |
10 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → 𝐴 ∈ 𝑈) |
11 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) |
12 | 3, 9, 10, 11 | fvmptd 6197 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → (𝑂‘𝐴) = (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓})) |
13 | 12 | dmeqd 5248 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → dom (𝑂‘𝐴) = dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓})) |
14 | 13 | eleq2d 2673 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) ↔ 〈𝐵, 𝐶〉 ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}))) |
15 | | dmoprabss 6640 |
. . . . . . . . 9
⊢ dom
{〈〈𝑏, 𝑐〉, 𝑧〉 ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {〈𝑑, 𝑒〉 ∣ 𝜓})} ⊆ (𝑆 × 𝑇) |
16 | 15 | sseli 3564 |
. . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ dom
{〈〈𝑏, 𝑐〉, 𝑧〉 ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {〈𝑑, 𝑒〉 ∣ 𝜓})} → 〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇)) |
17 | | bropfvvvv.oo |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) |
18 | 2, 17 | bropfvvvvlem 7143 |
. . . . . . . . 9
⊢
((〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))) |
19 | 18 | ex 449 |
. . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
20 | 16, 19 | syl 17 |
. . . . . . 7
⊢
(〈𝐵, 𝐶〉 ∈ dom
{〈〈𝑏, 𝑐〉, 𝑧〉 ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {〈𝑑, 𝑒〉 ∣ 𝜓})} → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
21 | | df-mpt2 6554 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) = {〈〈𝑏, 𝑐〉, 𝑧〉 ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {〈𝑑, 𝑒〉 ∣ 𝜓})} |
22 | 21 | dmeqi 5247 |
. . . . . . 7
⊢ dom
(𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) = dom {〈〈𝑏, 𝑐〉, 𝑧〉 ∣ ((𝑏 ∈ 𝑆 ∧ 𝑐 ∈ 𝑇) ∧ 𝑧 = {〈𝑑, 𝑒〉 ∣ 𝜓})} |
23 | 20, 22 | eleq2s 2706 |
. . . . . 6
⊢
(〈𝐵, 𝐶〉 ∈ dom (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
24 | 14, 23 | syl6bi 242 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
25 | 24 | com23 84 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
26 | 25 | a1d 25 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
27 | | ianor 508 |
. . . . 5
⊢ (¬
(𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) ↔ (¬ 𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V)) |
28 | 2 | fvmptndm 6216 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ∈ 𝑈 → (𝑂‘𝐴) = ∅) |
29 | 28 | dmeqd 5248 |
. . . . . . . . . 10
⊢ (¬
𝐴 ∈ 𝑈 → dom (𝑂‘𝐴) = dom ∅) |
30 | 29 | eleq2d 2673 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ 𝑈 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) ↔ 〈𝐵, 𝐶〉 ∈ dom ∅)) |
31 | | dm0 5260 |
. . . . . . . . . 10
⊢ dom
∅ = ∅ |
32 | 31 | eleq2i 2680 |
. . . . . . . . 9
⊢
(〈𝐵, 𝐶〉 ∈ dom ∅ ↔
〈𝐵, 𝐶〉 ∈ ∅) |
33 | 30, 32 | syl6bb 275 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ 𝑈 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) ↔ 〈𝐵, 𝐶〉 ∈ ∅)) |
34 | | noel 3878 |
. . . . . . . . 9
⊢ ¬
〈𝐵, 𝐶〉 ∈ ∅ |
35 | 34 | pm2.21i 115 |
. . . . . . . 8
⊢
(〈𝐵, 𝐶〉 ∈ ∅ →
(𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
36 | 33, 35 | syl6bi 242 |
. . . . . . 7
⊢ (¬
𝐴 ∈ 𝑈 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
37 | 36 | a1d 25 |
. . . . . 6
⊢ (¬
𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
38 | | notnotb 303 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑈 ↔ ¬ ¬ 𝐴 ∈ 𝑈) |
39 | | elex 3185 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝑋 → 𝑆 ∈ V) |
40 | | elex 3185 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑌 → 𝑇 ∈ V) |
41 | 39, 40 | anim12i 588 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑆 ∈ V ∧ 𝑇 ∈ V)) |
43 | | mpt2exga 7135 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ V ∧ 𝑇 ∈ V) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) |
45 | 44 | pm2.24d 146 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑈 ∧ (𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌)) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
46 | 45 | ex 449 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑈 → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))) |
47 | 46 | com23 84 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))) |
48 | 38, 47 | sylbir 224 |
. . . . . . 7
⊢ (¬
¬ 𝐴 ∈ 𝑈 → (¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))))) |
49 | 48 | imp 444 |
. . . . . 6
⊢ ((¬
¬ 𝐴 ∈ 𝑈 ∧ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
50 | 37, 49 | jaoi3 1003 |
. . . . 5
⊢ ((¬
𝐴 ∈ 𝑈 ∨ ¬ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
51 | 27, 50 | sylbi 206 |
. . . 4
⊢ (¬
(𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
52 | 51 | com34 89 |
. . 3
⊢ (¬
(𝐴 ∈ 𝑈 ∧ (𝑏 ∈ 𝑆, 𝑐 ∈ 𝑇 ↦ {〈𝑑, 𝑒〉 ∣ 𝜓}) ∈ V) → ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
53 | 26, 52 | pm2.61i 175 |
. 2
⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (〈𝐵, 𝐶〉 ∈ dom (𝑂‘𝐴) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
54 | 1, 53 | mpdi 44 |
1
⊢ ((𝑆 ∈ 𝑋 ∧ 𝑇 ∈ 𝑌) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |