This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brbigcup

Description: Binary relation over Bigcup . (Contributed by Scott Fenton, 11-Apr-2012)

Ref Expression
Hypothesis brbigcup.1 ⊢ B ∈ V
Assertion brbigcup ⊢ A 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ ⋃ A = B

Proof

Step Hyp Ref Expression
1 brbigcup.1 ⊢ B ∈ V
2 relbigcup ⊢ Rel ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉
3 2 brrelex1i ⊢ A 𝖡𝗂𝗀𝖼𝗎𝗉 B → A ∈ V
4 eleq1 ⊢ ⋃ A = B → ⋃ A ∈ V ↔ B ∈ V
5 1 4 mpbiri ⊢ ⋃ A = B → ⋃ A ∈ V
6 uniexb ⊢ A ∈ V ↔ ⋃ A ∈ V
7 5 6 sylibr ⊢ ⋃ A = B → A ∈ V
8 breq1 ⊢ x = A → x 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ A 𝖡𝗂𝗀𝖼𝗎𝗉 B
9 unieq ⊢ x = A → ⋃ x = ⋃ A
10 9 eqeq1d ⊢ x = A → ⋃ x = B ↔ ⋃ A = B
11 vex ⊢ x ∈ V
12 df-bigcup ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 = V × V ∖ ran ⁡ V ⊗ E ∆ E ∘ E ⊗ V
13 brxp ⊢ x V × V B ↔ x ∈ V ∧ B ∈ V
14 11 1 13 mpbir2an ⊢ x V × V B
15 epel ⊢ y E z ↔ y ∈ z
16 15 rexbii ⊢ ∃ z ∈ x y E z ↔ ∃ z ∈ x y ∈ z
17 vex ⊢ y ∈ V
18 17 11 coep ⊢ y E ∘ E x ↔ ∃ z ∈ x y E z
19 eluni2 ⊢ y ∈ ⋃ x ↔ ∃ z ∈ x y ∈ z
20 16 18 19 3bitr4ri ⊢ y ∈ ⋃ x ↔ y E ∘ E x
21 11 1 12 14 20 brtxpsd3 ⊢ x 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ B = ⋃ x
22 eqcom ⊢ B = ⋃ x ↔ ⋃ x = B
23 21 22 bitri ⊢ x 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ ⋃ x = B
24 8 10 23 vtoclbg ⊢ A ∈ V → A 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ ⋃ A = B
25 3 7 24 pm5.21nii ⊢ A 𝖡𝗂𝗀𝖼𝗎𝗉 B ↔ ⋃ A = B