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 ( 𝐵 , 𝐴 , 𝑅 ) = ∪ ( 𝐴 ∖ ( ( ◡ 𝑅 “ 𝐵 ) ∪ ( 𝑅 “ ( 𝐴 ∖ ( ◡ 𝑅 “ 𝐵 ) ) ) ) )