Metamath Proof Explorer

Theorem brcup

Description: Binary relation form of the Cup function. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brcup.1 ⊢ 𝐴 ∈ V
brcup.2 ⊢ 𝐵 ∈ V
brcup.3 ⊢ 𝐶 ∈ V
Assertion brcup ( ⟨ 𝐴 , 𝐵 ⟩ Cup 𝐶 ↔ 𝐶 = ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 brcup.1 ⊢ 𝐴 ∈ V
2 brcup.2 ⊢ 𝐵 ∈ V
3 brcup.3 ⊢ 𝐶 ∈ V
4 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5 df-cup ⊢ Cup = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⊗ V ) ) )
6 1 2 opelvv ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V )
7 brxp ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ( ( V × V ) × V ) 𝐶 ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ∧ 𝐶 ∈ V ) )
8 6 3 7 mpbir2an ⊢ ⟨ 𝐴 , 𝐵 ⟩ ( ( V × V ) × V ) 𝐶
9 epel ⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
10 vex ⊢ 𝑦 ∈ V
11 10 4 brcnv ⊢ ( 𝑦 ◡ 1st ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑦 )
12 1 2 br1steq ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ 1st 𝑦 ↔ 𝑦 = 𝐴 )
13 11 12 bitri ⊢ ( 𝑦 ◡ 1st ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑦 = 𝐴 )
14 9 13 anbi12ci ⊢ ( ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 1st ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
15 14 exbii ⊢ ( ∃ 𝑦 ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 1st ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
16 vex ⊢ 𝑥 ∈ V
17 16 4 brco ⊢ ( 𝑥 ( ◡ 1st ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑦 ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 1st ⟨ 𝐴 , 𝐵 ⟩ ) )
18 1 clel3 ⊢ ( 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
19 15 17 18 3bitr4i ⊢ ( 𝑥 ( ◡ 1st ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ∈ 𝐴 )
20 10 4 brcnv ⊢ ( 𝑦 ◡ 2nd ⟨ 𝐴 , 𝐵 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑦 )
21 1 2 br2ndeq ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ 2nd 𝑦 ↔ 𝑦 = 𝐵 )
22 20 21 bitri ⊢ ( 𝑦 ◡ 2nd ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑦 = 𝐵 )
23 9 22 anbi12ci ⊢ ( ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 2nd ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) )
24 23 exbii ⊢ ( ∃ 𝑦 ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 2nd ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) )
25 16 4 brco ⊢ ( 𝑥 ( ◡ 2nd ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑦 ( 𝑥 E 𝑦 ∧ 𝑦 ◡ 2nd ⟨ 𝐴 , 𝐵 ⟩ ) )
26 2 clel3 ⊢ ( 𝑥 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 = 𝐵 ∧ 𝑥 ∈ 𝑦 ) )
27 24 25 26 3bitr4i ⊢ ( 𝑥 ( ◡ 2nd ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ∈ 𝐵 )
28 19 27 orbi12i ⊢ ( ( 𝑥 ( ◡ 1st ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝑥 ( ◡ 2nd ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
29 brun ⊢ ( 𝑥 ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 ( ◡ 1st ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ∨ 𝑥 ( ◡ 2nd ∘ E ) ⟨ 𝐴 , 𝐵 ⟩ ) )
30 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
31 28 29 30 3bitr4ri ⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ( ( ◡ 1st ∘ E ) ∪ ( ◡ 2nd ∘ E ) ) ⟨ 𝐴 , 𝐵 ⟩ )
32 4 3 5 8 31 brtxpsd3 ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ Cup 𝐶 ↔ 𝐶 = ( 𝐴 ∪ 𝐵 ) )