| Step | Hyp | Ref
| Expression |
| 1 | | df-br 5144 |
. 2
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷)) |
| 2 | | relco 6126 |
. . . 4
⊢ Rel
(𝐶 ∘ 𝐷) |
| 3 | 2 | brrelex12i 5740 |
. . 3
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 4 | | snprc 4717 |
. . . . . 6
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
| 5 | | noel 4338 |
. . . . . . 7
⊢ ¬
𝐵 ∈
∅ |
| 6 | | imaeq2 6074 |
. . . . . . . . . 10
⊢ ({𝐴} = ∅ → (𝐷 “ {𝐴}) = (𝐷 “ ∅)) |
| 7 | 6 | imaeq2d 6078 |
. . . . . . . . 9
⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = (𝐶 “ (𝐷 “ ∅))) |
| 8 | | ima0 6095 |
. . . . . . . . . . 11
⊢ (𝐷 “ ∅) =
∅ |
| 9 | 8 | imaeq2i 6076 |
. . . . . . . . . 10
⊢ (𝐶 “ (𝐷 “ ∅)) = (𝐶 “ ∅) |
| 10 | | ima0 6095 |
. . . . . . . . . 10
⊢ (𝐶 “ ∅) =
∅ |
| 11 | 9, 10 | eqtri 2765 |
. . . . . . . . 9
⊢ (𝐶 “ (𝐷 “ ∅)) =
∅ |
| 12 | 7, 11 | eqtrdi 2793 |
. . . . . . . 8
⊢ ({𝐴} = ∅ → (𝐶 “ (𝐷 “ {𝐴})) = ∅) |
| 13 | 12 | eleq2d 2827 |
. . . . . . 7
⊢ ({𝐴} = ∅ → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ 𝐵 ∈ ∅)) |
| 14 | 5, 13 | mtbiri 327 |
. . . . . 6
⊢ ({𝐴} = ∅ → ¬ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
| 15 | 4, 14 | sylbi 217 |
. . . . 5
⊢ (¬
𝐴 ∈ V → ¬
𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
| 16 | 15 | con4i 114 |
. . . 4
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐴 ∈ V) |
| 17 | | elex 3501 |
. . . 4
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → 𝐵 ∈ V) |
| 18 | 16, 17 | jca 511 |
. . 3
⊢ (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
| 19 | | df-rex 3071 |
. . . . 5
⊢
(∃𝑧 ∈
(𝐷 “ {𝐴})𝑧𝐶𝐵 ↔ ∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵)) |
| 20 | | elimasng 6107 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ V ∧ 𝑧 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 〈𝐴, 𝑧〉 ∈ 𝐷)) |
| 21 | 20 | elvd 3486 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 〈𝐴, 𝑧〉 ∈ 𝐷)) |
| 22 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝐴𝐷𝑧 ↔ 〈𝐴, 𝑧〉 ∈ 𝐷) |
| 23 | 21, 22 | bitr4di 289 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧)) |
| 24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝑧 ∈ (𝐷 “ {𝐴}) ↔ 𝐴𝐷𝑧)) |
| 25 | 24 | anbi1d 631 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ (𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
| 26 | 25 | exbidv 1921 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝑧 ∈ (𝐷 “ {𝐴}) ∧ 𝑧𝐶𝐵) ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
| 27 | 19, 26 | bitr2id 284 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
| 28 | | brcog 5877 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ ∃𝑧(𝐴𝐷𝑧 ∧ 𝑧𝐶𝐵))) |
| 29 | | elimag 6082 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
| 30 | 29 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})) ↔ ∃𝑧 ∈ (𝐷 “ {𝐴})𝑧𝐶𝐵)) |
| 31 | 27, 28, 30 | 3bitr4d 311 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴})))) |
| 32 | 3, 18, 31 | pm5.21nii 378 |
. 2
⊢ (𝐴(𝐶 ∘ 𝐷)𝐵 ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |
| 33 | 1, 32 | bitr3i 277 |
1
⊢
(〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) |