Metamath Proof Explorer

Theorem brub

Description: Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018)

Ref Expression
Hypotheses brub.1 ⊢ S ∈ V
brub.2 ⊢ A ∈ V
Assertion brub ⊢ S UB R A ↔ ∀ x ∈ S x R A

Proof

Step Hyp Ref Expression
1 brub.1 ⊢ S ∈ V
2 brub.2 ⊢ A ∈ V
3 brxp ⊢ S V × V A ↔ S ∈ V ∧ A ∈ V
4 1 2 3 mpbir2an ⊢ S V × V A
5 brdif ⊢ S V × V ∖ V ∖ R ∘ E -1 A ↔ S V × V A ∧ ¬ S V ∖ R ∘ E -1 A
6 4 5 mpbiran ⊢ S V × V ∖ V ∖ R ∘ E -1 A ↔ ¬ S V ∖ R ∘ E -1 A
7 1 2 coepr ⊢ S V ∖ R ∘ E -1 A ↔ ∃ x ∈ S x V ∖ R A
8 6 7 xchbinx ⊢ S V × V ∖ V ∖ R ∘ E -1 A ↔ ¬ ∃ x ∈ S x V ∖ R A
9 df-ub ⊢ UB R = V × V ∖ V ∖ R ∘ E -1
10 9 breqi ⊢ S UB R A ↔ S V × V ∖ V ∖ R ∘ E -1 A
11 brv ⊢ x V A
12 brdif ⊢ x V ∖ R A ↔ x V A ∧ ¬ x R A
13 11 12 mpbiran ⊢ x V ∖ R A ↔ ¬ x R A
14 13 rexbii ⊢ ∃ x ∈ S x V ∖ R A ↔ ∃ x ∈ S ¬ x R A
15 rexnal ⊢ ∃ x ∈ S ¬ x R A ↔ ¬ ∀ x ∈ S x R A
16 14 15 bitri ⊢ ∃ x ∈ S x V ∖ R A ↔ ¬ ∀ x ∈ S x R A
17 16 con2bii ⊢ ∀ x ∈ S x R A ↔ ¬ ∃ x ∈ S x V ∖ R A
18 8 10 17 3bitr4i ⊢ S UB R A ↔ ∀ x ∈ S x R A