Theorem dfso2 31644

Description: Quantifier free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013.)

Assertion

Ref	Expression
dfso2	|- ( R Or A <-> ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) )

Proof of Theorem dfso2

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-so 5036	. 2 |- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
2		opelxp 5146	. . . . . 6 |- ( <. x , y >. e. ( A X. A ) <-> ( x e. A /\ y e. A ) )
3		brun 4703	. . . . . . . . . 10 |- ( x ( _I u. `' R ) y <-> ( x _I y \/ x `' R y ) )
4		vex 3203	. . . . . . . . . . . 12 |- y e. _V
5	4	ideq 5274	. . . . . . . . . . 11 |- ( x _I y <-> x = y )
6		vex 3203	. . . . . . . . . . . 12 |- x e. _V
7	6, 4	brcnv 5305	. . . . . . . . . . 11 |- ( x `' R y <-> y R x )
8	5, 7	orbi12i 543	. . . . . . . . . 10 |- ( ( x _I y \/ x `' R y ) <-> ( x = y \/ y R x ) )
9	3, 8	bitr2i 265	. . . . . . . . 9 |- ( ( x = y \/ y R x ) <-> x ( _I u. `' R ) y )
10	9	orbi2i 541	. . . . . . . 8 |- ( ( x R y \/ ( x = y \/ y R x ) ) <-> ( x R y \/ x ( _I u. `' R ) y ) )
11		3orass 1040	. . . . . . . 8 |- ( ( x R y \/ x = y \/ y R x ) <-> ( x R y \/ ( x = y \/ y R x ) ) )
12		brun 4703	. . . . . . . 8 |- ( x ( R u. ( _I u. `' R ) ) y <-> ( x R y \/ x ( _I u. `' R ) y ) )
13	10, 11, 12	3bitr4i 292	. . . . . . 7 |- ( ( x R y \/ x = y \/ y R x ) <-> x ( R u. ( _I u. `' R ) ) y )
14		df-br 4654	. . . . . . 7 |- ( x ( R u. ( _I u. `' R ) ) y <-> <. x , y >. e. ( R u. ( _I u. `' R ) ) )
15	13, 14	bitr2i 265	. . . . . 6 |- ( <. x , y >. e. ( R u. ( _I u. `' R ) ) <-> ( x R y \/ x = y \/ y R x ) )
16	2, 15	imbi12i 340	. . . . 5 |- ( ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) <-> ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
17	16	2albii 1748	. . . 4 |- ( A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
18		relxp 5227	. . . . 5 |- Rel ( A X. A )
19		ssrel 5207	. . . . 5 |- ( Rel ( A X. A ) -> ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) ) )
20	18, 19	ax-mp 5	. . . 4 |- ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x A. y ( <. x , y >. e. ( A X. A ) -> <. x , y >. e. ( R u. ( _I u. `' R ) ) ) )
21		r2al 2939	. . . 4 |- ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) ) )
22	17, 20, 21	3bitr4i 292	. . 3 |- ( ( A X. A ) C_ ( R u. ( _I u. `' R ) ) <-> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )
23	22	anbi2i 730	. 2 |- ( ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
24	1, 23	bitr4i 267	1 |- ( R Or A <-> ( R Po A /\ ( A X. A ) C_ ( R u. ( _I u. `' R ) ) ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   \/ w3o 1036   A.wal 1481   e. wcel 1990   A.wral 2912   u. cun 3572   C_ wss 3574   <.cop 4183   class class class wbr 4653   _I cid 5023   Po wpo 5033   Or wor 5034   X. cxp 5112   `'ccnv 5113   Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-id 5024  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122

This theorem is referenced by: (None)