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

Metamath Proof Explorer

Theorem dfsup2

Description: Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion dfsup2 sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-sup ⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) }
2 dfrab3 ⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } )
3 eqabcb ⊢ ( { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ∀ 𝑥 ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) )
4 vex ⊢ 𝑥 ∈ V
5 eldif ⊢ ( 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) )
6 4 5 mpbiran ⊢ ( 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ↔ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
7 4 elima ⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝑅 𝑥 )
8 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝑅 𝑥 ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 )
9 7 8 bitri ⊢ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 )
10 4 elima ⊢ ( 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ↔ ∃ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) 𝑦 𝑅 𝑥 )
11 dfrex2 ⊢ ( ∃ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) 𝑦 𝑅 𝑥 ↔ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 )
12 10 11 bitri ⊢ ( 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ↔ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 )
13 9 12 orbi12i ⊢ ( ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ∨ 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ( ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∨ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) )
14 elun ⊢ ( 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ( 𝑥 ∈ ( ◡ 𝑅 “ 𝐵 ) ∨ 𝑥 ∈ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
15 ianor ⊢ ( ¬ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ( ¬ ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∨ ¬ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) )
16 13 14 15 3bitr4i ⊢ ( 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ↔ ¬ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) )
17 16 con2bii ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 ∈ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
18 vex ⊢ 𝑦 ∈ V
19 18 4 brcnv ⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
20 19 notbii ⊢ ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 )
21 20 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 )
22 impexp ⊢ ( ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) )
23 eldif ⊢ ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) )
24 23 imbi1i ⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) )
25 18 elima ⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑧 ◡ 𝑅 𝑦 )
26 vex ⊢ 𝑧 ∈ V
27 26 18 brcnv ⊢ ( 𝑧 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑧 )
28 27 rexbii ⊢ ( ∃ 𝑧 ∈ 𝐵 𝑧 ◡ 𝑅 𝑦 ↔ ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 )
29 25 28 bitri ⊢ ( 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 )
30 29 imbi2i ⊢ ( ( 𝑦 𝑅 𝑥 → 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
31 con34b ⊢ ( ( 𝑦 𝑅 𝑥 → 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) ) ↔ ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) )
32 30 31 bitr3i ⊢ ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) )
33 32 imbi2i ⊢ ( ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( 𝑦 ∈ 𝐴 → ( ¬ 𝑦 ∈ ( ◡ 𝑅 “ 𝐵 ) → ¬ 𝑦 𝑅 𝑥 ) ) )
34 22 24 33 3bitr4i ⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) → ¬ 𝑦 𝑅 𝑥 ) ↔ ( 𝑦 ∈ 𝐴 → ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
35 34 ralbii2 ⊢ ( ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) )
36 21 35 anbi12i ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 ◡ 𝑅 𝑥 ∧ ∀ 𝑦 ∈ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ¬ 𝑦 𝑅 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) )
37 6 17 36 3bitr2ri ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ 𝑥 ∈ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) )
38 3 37 mpgbir ⊢ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
39 38 ineq2i ⊢ ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ) = ( 𝐴 ∩ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) )
40 invdif ⊢ ( 𝐴 ∩ ( V ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) ) ) = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
41 39 40 eqtri ⊢ ( 𝐴 ∩ { 𝑥 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ) = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
42 2 41 eqtri ⊢ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
43 42 unieqi ⊢ ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )
44 1 43 eqtri ⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )