| Step | Hyp | Ref
| Expression |
| 1 | | refrel 23516 |
. . . 4
⊢ Rel
Ref |
| 2 | 1 | brrelex2i 5742 |
. . 3
⊢ (𝐴Ref𝐵 → 𝐵 ∈ V) |
| 3 | 2 | anim2i 617 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐴Ref𝐵) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
| 4 | | simpl 482 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐴 ∈ 𝐶) |
| 5 | | simpr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝑌 = 𝑋) |
| 6 | | isref.2 |
. . . . . . 7
⊢ 𝑌 = ∪
𝐵 |
| 7 | | isref.1 |
. . . . . . 7
⊢ 𝑋 = ∪
𝐴 |
| 8 | 5, 6, 7 | 3eqtr3g 2800 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 = ∪
𝐴) |
| 9 | | uniexg 7760 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ∪ 𝐴 ∈ V) |
| 10 | 9 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐴 ∈ V) |
| 11 | 8, 10 | eqeltrd 2841 |
. . . . 5
⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → ∪ 𝐵 ∈ V) |
| 12 | | uniexb 7784 |
. . . . 5
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) |
| 13 | 11, 12 | sylibr 234 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 ∧ 𝑌 = 𝑋) → 𝐵 ∈ V) |
| 14 | 13 | adantrr 717 |
. . 3
⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → 𝐵 ∈ V) |
| 15 | 4, 14 | jca 511 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) → (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V)) |
| 16 | | unieq 4918 |
. . . . . 6
⊢ (𝑎 = 𝐴 → ∪ 𝑎 = ∪
𝐴) |
| 17 | 16, 7 | eqtr4di 2795 |
. . . . 5
⊢ (𝑎 = 𝐴 → ∪ 𝑎 = 𝑋) |
| 18 | 17 | eqeq2d 2748 |
. . . 4
⊢ (𝑎 = 𝐴 → (∪ 𝑏 = ∪
𝑎 ↔ ∪ 𝑏 =
𝑋)) |
| 19 | | raleq 3323 |
. . . 4
⊢ (𝑎 = 𝐴 → (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)) |
| 20 | 18, 19 | anbi12d 632 |
. . 3
⊢ (𝑎 = 𝐴 → ((∪ 𝑏 = ∪
𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦))) |
| 21 | | unieq 4918 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ∪ 𝑏 = ∪
𝐵) |
| 22 | 21, 6 | eqtr4di 2795 |
. . . . 5
⊢ (𝑏 = 𝐵 → ∪ 𝑏 = 𝑌) |
| 23 | 22 | eqeq1d 2739 |
. . . 4
⊢ (𝑏 = 𝐵 → (∪ 𝑏 = 𝑋 ↔ 𝑌 = 𝑋)) |
| 24 | | rexeq 3322 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
| 25 | 24 | ralbidv 3178 |
. . . 4
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦)) |
| 26 | 23, 25 | anbi12d 632 |
. . 3
⊢ (𝑏 = 𝐵 → ((∪ 𝑏 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦) ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
| 27 | | df-ref 23513 |
. . 3
⊢ Ref =
{〈𝑎, 𝑏〉 ∣ (∪ 𝑏 =
∪ 𝑎 ∧ ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝑥 ⊆ 𝑦)} |
| 28 | 20, 26, 27 | brabg 5544 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ V) → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |
| 29 | 3, 15, 28 | pm5.21nd 802 |
1
⊢ (𝐴 ∈ 𝐶 → (𝐴Ref𝐵 ↔ (𝑌 = 𝑋 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦))) |