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 abeq1 ( { 𝑥 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) } = ( 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 ( 𝐵 , 𝐴 , 𝑅 ) = ( 𝐴 ∖ ( ( 𝑅𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( 𝑅𝐵 ) ) ) ) )