Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. 2
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷)) |
2 | | relco 5550 |
. . . 4
⊢ Rel
(𝐶 ∘ 𝐷) |
3 | | brrelex12 5079 |
. . . 4
⊢ ((Rel
(𝐶 ∘ 𝐷) ∧ 𝐴(𝐶 ∘ 𝐷)𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
4 | 2, 3 | mpan 702 |
. . 3
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
5 | | snprc 4197 |
. . . . . 6
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
6 | | noel 3878 |
. . . . . . 7
⊢ ¬
𝐵 ∈
∅ |
7 | | imaeq2 5381 |
. . . . . . . . . 10
⊢ ({𝐴} = ∅ → (𝐷 “ {𝐴}) = (𝐷 “ ∅)) |
8 | 7 | imaeq2d 5385 |
. . . . . . . . 9
⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = (𝐶 “ (𝐷 “ ∅))) |
9 | | ima0 5400 |
. . . . . . . . . . 11
⊢ (𝐷 “ ∅) =
∅ |
10 | 9 | imaeq2i 5383 |
. . . . . . . . . 10
⊢ (𝐶 “ (𝐷 “ ∅)) = (𝐶 “ ∅) |
11 | | ima0 5400 |
. . . . . . . . . 10
⊢ (𝐶 “ ∅) =
∅ |
12 | 10, 11 | eqtri 2632 |
. . . . . . . . 9
⊢ (𝐶 “ (𝐷 “ ∅)) =
∅ |
13 | 8, 12 | syl6eq 2660 |
. . . . . . . 8
⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = ∅) |
14 | 13 | eleq2d 2673 |
. . . . . . 7
⊢ ({𝐴} = ∅ → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ 𝐵 ∈ ∅)) |
15 | 6, 14 | mtbiri 316 |
. . . . . 6
⊢ ({𝐴} = ∅ → ¬ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
16 | 5, 15 | sylbi 206 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
17 | 16 | con4i 112 |
. . . 4
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐴 ∈ V) |
18 | | elex 3185 |
. . . 4
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐵 ∈ V) |
19 | 17, 18 | jca 553 |
. . 3
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
20 | | df-rex 2902 |
. . . . 5
⊢
(∃𝑧 ∈
(𝐷 “ {𝐴})𝑧𝐶𝐵 ↔ ∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵)) |
21 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
22 | | elimasng 5410 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 〈𝐴, 𝑧〉 ∈ 𝐷)) |
23 | 21, 22 | mpan2 703 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 〈𝐴, 𝑧〉 ∈ 𝐷)) |
24 | | df-br 4584 |
. . . . . . . . 9
⊢ (𝐴𝐷𝑧 ↔ 〈𝐴, 𝑧〉 ∈ 𝐷) |
25 | 23, 24 | syl6bbr 277 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧)) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧)) |
27 | 26 | anbi1d 737 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ (𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
28 | 27 | exbidv 1837 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
29 | 20, 28 | syl5rbb 272 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
30 | | brcog 5210 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
31 | | elimag 5389 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
32 | 31 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
33 | 29, 30, 32 | 3bitr4d 299 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))) |
34 | 4, 19, 33 | pm5.21nii 367 |
. 2
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
35 | 1, 34 | bitr3i 265 |
1
⊢
(〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |