Proof of Theorem bropfvvvvlem
Step | Hyp | Ref
| Expression |
1 | | opelxp 5587 |
. . 3
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) ↔ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)) |
2 | | brne0 5103 |
. . . . . . 7
⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐵(𝑂‘𝐴)𝐶) ≠ ∅) |
3 | | bropfvvvv.oo |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) |
4 | 3 | 3expb 1122 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)) → (𝐵(𝑂‘𝐴)𝐶) = {〈𝑑, 𝑒〉 ∣ 𝜃}) |
5 | 4 | breqd 5064 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 ↔ 𝐷{〈𝑑, 𝑒〉 ∣ 𝜃}𝐸)) |
6 | | brabv 5448 |
. . . . . . . . . . . . . . 15
⊢ (𝐷{〈𝑑, 𝑒〉 ∣ 𝜃}𝐸 → (𝐷 ∈ V ∧ 𝐸 ∈ V)) |
7 | 6 | anim2i 620 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐷{〈𝑑, 𝑒〉 ∣ 𝜃}𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))) |
8 | 7 | ex 416 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑈 → (𝐷{〈𝑑, 𝑒〉 ∣ 𝜃}𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
9 | 8 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)) → (𝐷{〈𝑑, 𝑒〉 ∣ 𝜃}𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
10 | 5, 9 | sylbid 243 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
11 | 10 | ex 416 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑈 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
12 | 11 | com23 86 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑈 → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
13 | 12 | a1d 25 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑈 → ((𝐵(𝑂‘𝐴)𝐶) ≠ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
14 | | bropfvvvv.o |
. . . . . . . . . 10
⊢ 𝑂 = (𝑎 ∈ 𝑈 ↦ (𝑏 ∈ 𝑉, 𝑐 ∈ 𝑊 ↦ {〈𝑑, 𝑒〉 ∣ 𝜑})) |
15 | 14 | fvmptndm 6848 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ 𝑈 → (𝑂‘𝐴) = ∅) |
16 | | df-ov 7216 |
. . . . . . . . . . 11
⊢ (𝐵(𝑂‘𝐴)𝐶) = ((𝑂‘𝐴)‘〈𝐵, 𝐶〉) |
17 | | fveq1 6716 |
. . . . . . . . . . 11
⊢ ((𝑂‘𝐴) = ∅ → ((𝑂‘𝐴)‘〈𝐵, 𝐶〉) = (∅‘〈𝐵, 𝐶〉)) |
18 | 16, 17 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝑂‘𝐴) = ∅ → (𝐵(𝑂‘𝐴)𝐶) = (∅‘〈𝐵, 𝐶〉)) |
19 | | 0fv 6756 |
. . . . . . . . . 10
⊢
(∅‘〈𝐵, 𝐶〉) = ∅ |
20 | 18, 19 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝑂‘𝐴) = ∅ → (𝐵(𝑂‘𝐴)𝐶) = ∅) |
21 | | eqneqall 2951 |
. . . . . . . . 9
⊢ ((𝐵(𝑂‘𝐴)𝐶) = ∅ → ((𝐵(𝑂‘𝐴)𝐶) ≠ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
22 | 15, 20, 21 | 3syl 18 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ 𝑈 → ((𝐵(𝑂‘𝐴)𝐶) ≠ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))))) |
23 | 13, 22 | pm2.61i 185 |
. . . . . . 7
⊢ ((𝐵(𝑂‘𝐴)𝐶) ≠ ∅ → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))))) |
24 | 2, 23 | mpcom 38 |
. . . . . 6
⊢ (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
25 | 24 | com12 32 |
. . . . 5
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
26 | 25 | anc2ri 560 |
. . . 4
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → ((𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)) ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇)))) |
27 | | 3anan32 1099 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)) ↔ ((𝐴 ∈ 𝑈 ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)) ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇))) |
28 | 26, 27 | syl6ibr 255 |
. . 3
⊢ ((𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
29 | 1, 28 | sylbi 220 |
. 2
⊢
(〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) → (𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸 → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V)))) |
30 | 29 | imp 410 |
1
⊢
((〈𝐵, 𝐶〉 ∈ (𝑆 × 𝑇) ∧ 𝐷(𝐵(𝑂‘𝐴)𝐶)𝐸) → (𝐴 ∈ 𝑈 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ (𝐷 ∈ V ∧ 𝐸 ∈ V))) |