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 𝑅 𝐴 ↔ ∀ 𝑥 ∈ 𝑆 𝑥 𝑅 𝐴 )