Step | Hyp | Ref
| Expression |
1 | | fnerel 34165 |
. . . . 5
⊢ Rel
Fne |
2 | 1 | brrelex1i 5579 |
. . . 4
⊢ (𝐴Fne𝐵 → 𝐴 ∈ V) |
3 | 2 | anim1i 618 |
. . 3
⊢ ((𝐴Fne𝐵 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) |
4 | 3 | ancoms 462 |
. 2
⊢ ((𝐵 ∈ 𝐶 ∧ 𝐴Fne𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) |
5 | | simpr 488 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → 𝑋 = 𝑌) |
6 | | isfne.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐴 |
7 | | isfne.2 |
. . . . 5
⊢ 𝑌 = ∪
𝐵 |
8 | 5, 6, 7 | 3eqtr3g 2796 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → ∪ 𝐴 = ∪
𝐵) |
9 | | simpr 488 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐴 =
∪ 𝐵) |
10 | | uniexg 7484 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝐶 → ∪ 𝐵 ∈ V) |
11 | 10 | adantr 484 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐵
∈ V) |
12 | 9, 11 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → ∪ 𝐴
∈ V) |
13 | | uniexb 7505 |
. . . . . 6
⊢ (𝐴 ∈ V ↔ ∪ 𝐴
∈ V) |
14 | 12, 13 | sylibr 237 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → 𝐴 ∈ V) |
15 | | simpl 486 |
. . . . 5
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → 𝐵 ∈ 𝐶) |
16 | 14, 15 | jca 515 |
. . . 4
⊢ ((𝐵 ∈ 𝐶 ∧ ∪ 𝐴 = ∪
𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) |
17 | 8, 16 | syldan 594 |
. . 3
⊢ ((𝐵 ∈ 𝐶 ∧ 𝑋 = 𝑌) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) |
18 | 17 | adantrr 717 |
. 2
⊢ ((𝐵 ∈ 𝐶 ∧ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) → (𝐴 ∈ V ∧ 𝐵 ∈ 𝐶)) |
19 | | unieq 4807 |
. . . . . 6
⊢ (𝑟 = 𝐴 → ∪ 𝑟 = ∪
𝐴) |
20 | 19, 6 | eqtr4di 2791 |
. . . . 5
⊢ (𝑟 = 𝐴 → ∪ 𝑟 = 𝑋) |
21 | 20 | eqeq1d 2740 |
. . . 4
⊢ (𝑟 = 𝐴 → (∪ 𝑟 = ∪
𝑠 ↔ 𝑋 = ∪ 𝑠)) |
22 | | raleq 3310 |
. . . 4
⊢ (𝑟 = 𝐴 → (∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥))) |
23 | 21, 22 | anbi12d 634 |
. . 3
⊢ (𝑟 = 𝐴 → ((∪ 𝑟 = ∪
𝑠 ∧ ∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)) ↔ (𝑋 = ∪ 𝑠 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)))) |
24 | | unieq 4807 |
. . . . . 6
⊢ (𝑠 = 𝐵 → ∪ 𝑠 = ∪
𝐵) |
25 | 24, 7 | eqtr4di 2791 |
. . . . 5
⊢ (𝑠 = 𝐵 → ∪ 𝑠 = 𝑌) |
26 | 25 | eqeq2d 2749 |
. . . 4
⊢ (𝑠 = 𝐵 → (𝑋 = ∪ 𝑠 ↔ 𝑋 = 𝑌)) |
27 | | ineq1 4096 |
. . . . . . 7
⊢ (𝑠 = 𝐵 → (𝑠 ∩ 𝒫 𝑥) = (𝐵 ∩ 𝒫 𝑥)) |
28 | 27 | unieqd 4810 |
. . . . . 6
⊢ (𝑠 = 𝐵 → ∪ (𝑠 ∩ 𝒫 𝑥) = ∪
(𝐵 ∩ 𝒫 𝑥)) |
29 | 28 | sseq2d 3909 |
. . . . 5
⊢ (𝑠 = 𝐵 → (𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) |
30 | 29 | ralbidv 3109 |
. . . 4
⊢ (𝑠 = 𝐵 → (∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥) ↔ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥))) |
31 | 26, 30 | anbi12d 634 |
. . 3
⊢ (𝑠 = 𝐵 → ((𝑋 = ∪ 𝑠 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥)) ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) |
32 | | df-fne 34164 |
. . 3
⊢ Fne =
{〈𝑟, 𝑠〉 ∣ (∪ 𝑟 =
∪ 𝑠 ∧ ∀𝑥 ∈ 𝑟 𝑥 ⊆ ∪ (𝑠 ∩ 𝒫 𝑥))} |
33 | 23, 31, 32 | brabg 5394 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝐶) → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) |
34 | 4, 18, 33 | pm5.21nd 802 |
1
⊢ (𝐵 ∈ 𝐶 → (𝐴Fne𝐵 ↔ (𝑋 = 𝑌 ∧ ∀𝑥 ∈ 𝐴 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)))) |