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

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 ⊢ 𝑆 ∈ V
brub.2 ⊢ 𝐴 ∈ V
Assertion brub ( 𝑆 UB 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝑥 𝑅 𝐴 )

Proof

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