Theorem dfon2lem5 31692

Description: Lemma for dfon2 31697. Two sets satisfying the new definition also satisfy trichotomy with respect to e.. (Contributed by Scott Fenton, 25-Feb-2011.)

Hypotheses

Ref	Expression
dfon2lem5.1	|- A e. _V
dfon2lem5.2	|- B e. _V

Assertion

Ref	Expression
dfon2lem5	|- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A e. B \/ A = B \/ B e. A ) )

Distinct variable groups:   x, A, y   x, B, y

Proof of Theorem dfon2lem5

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfon2lem5.1	. . . 4 |- A e. _V
2		dfon2lem5.2	. . . 4 |- B e. _V
3	1, 2	dfon2lem4 31691	. . 3 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A C_ B \/ B C_ A ) )
4		dfpss2 3692	. . . . . 6 |- ( A C. B <-> ( A C_ B /\ -. A = B ) )
5		dfpss2 3692	. . . . . . 7 |- ( B C. A <-> ( B C_ A /\ -. B = A ) )
6		eqcom 2629	. . . . . . . . 9 |- ( B = A <-> A = B )
7	6	notbii 310	. . . . . . . 8 |- ( -. B = A <-> -. A = B )
8	7	anbi2i 730	. . . . . . 7 |- ( ( B C_ A /\ -. B = A ) <-> ( B C_ A /\ -. A = B ) )
9	5, 8	bitri 264	. . . . . 6 |- ( B C. A <-> ( B C_ A /\ -. A = B ) )
10	4, 9	orbi12i 543	. . . . 5 |- ( ( A C. B \/ B C. A ) <-> ( ( A C_ B /\ -. A = B ) \/ ( B C_ A /\ -. A = B ) ) )
11		andir 912	. . . . 5 |- ( ( ( A C_ B \/ B C_ A ) /\ -. A = B ) <-> ( ( A C_ B /\ -. A = B ) \/ ( B C_ A /\ -. A = B ) ) )
12	10, 11	bitr4i 267	. . . 4 |- ( ( A C. B \/ B C. A ) <-> ( ( A C_ B \/ B C_ A ) /\ -. A = B ) )
13		orcom 402	. . . . 5 |- ( ( A C. B \/ B C. A ) <-> ( B C. A \/ A C. B ) )
14		dfon2lem3 31690	. . . . . . . . 9 |- ( B e. _V -> ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) ) )
15	2, 14	ax-mp 5	. . . . . . . 8 |- ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) )
16	15	simpld 475	. . . . . . 7 |- ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> Tr B )
17		psseq1 3694	. . . . . . . . . . . 12 |- ( x = B -> ( x C. A <-> B C. A ) )
18		treq 4758	. . . . . . . . . . . 12 |- ( x = B -> ( Tr x <-> Tr B ) )
19	17, 18	anbi12d 747	. . . . . . . . . . 11 |- ( x = B -> ( ( x C. A /\ Tr x ) <-> ( B C. A /\ Tr B ) ) )
20		eleq1 2689	. . . . . . . . . . 11 |- ( x = B -> ( x e. A <-> B e. A ) )
21	19, 20	imbi12d 334	. . . . . . . . . 10 |- ( x = B -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( B C. A /\ Tr B ) -> B e. A ) ) )
22	2, 21	spcv 3299	. . . . . . . . 9 |- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( B C. A /\ Tr B ) -> B e. A ) )
23	22	expcomd 454	. . . . . . . 8 |- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr B -> ( B C. A -> B e. A ) ) )
24	23	imp 445	. . . . . . 7 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ Tr B ) -> ( B C. A -> B e. A ) )
25	16, 24	sylan2 491	. . . . . 6 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( B C. A -> B e. A ) )
26		dfon2lem3 31690	. . . . . . . . 9 |- ( A e. _V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )
27	1, 26	ax-mp 5	. . . . . . . 8 |- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) )
28	27	simpld 475	. . . . . . 7 |- ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> Tr A )
29		psseq1 3694	. . . . . . . . . . 11 |- ( y = A -> ( y C. B <-> A C. B ) )
30		treq 4758	. . . . . . . . . . 11 |- ( y = A -> ( Tr y <-> Tr A ) )
31	29, 30	anbi12d 747	. . . . . . . . . 10 |- ( y = A -> ( ( y C. B /\ Tr y ) <-> ( A C. B /\ Tr A ) ) )
32		eleq1 2689	. . . . . . . . . 10 |- ( y = A -> ( y e. B <-> A e. B ) )
33	31, 32	imbi12d 334	. . . . . . . . 9 |- ( y = A -> ( ( ( y C. B /\ Tr y ) -> y e. B ) <-> ( ( A C. B /\ Tr A ) -> A e. B ) ) )
34	1, 33	spcv 3299	. . . . . . . 8 |- ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( ( A C. B /\ Tr A ) -> A e. B ) )
35	34	expcomd 454	. . . . . . 7 |- ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr A -> ( A C. B -> A e. B ) ) )
36	28, 35	mpan9 486	. . . . . 6 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A C. B -> A e. B ) )
37	25, 36	orim12d 883	. . . . 5 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( B C. A \/ A C. B ) -> ( B e. A \/ A e. B ) ) )
38	13, 37	syl5bi 232	. . . 4 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A C. B \/ B C. A ) -> ( B e. A \/ A e. B ) ) )
39	12, 38	syl5bir 233	. . 3 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( ( A C_ B \/ B C_ A ) /\ -. A = B ) -> ( B e. A \/ A e. B ) ) )
40	3, 39	mpand 711	. 2 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( -. A = B -> ( B e. A \/ A e. B ) ) )
41		3orrot 1044	. . 3 |- ( ( A e. B \/ A = B \/ B e. A ) <-> ( A = B \/ B e. A \/ A e. B ) )
42		3orass 1040	. . . 4 |- ( ( A = B \/ B e. A \/ A e. B ) <-> ( A = B \/ ( B e. A \/ A e. B ) ) )
43		df-or 385	. . . 4 |- ( ( A = B \/ ( B e. A \/ A e. B ) ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
44	42, 43	bitri 264	. . 3 |- ( ( A = B \/ B e. A \/ A e. B ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
45	41, 44	bitri 264	. 2 |- ( ( A e. B \/ A = B \/ B e. A ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
46	40, 45	sylibr 224	1 |- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A e. B \/ A = B \/ B e. A ) )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383   /\ wa 384   \/ w3o 1036   A.wal 1481   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   C_ wss 3574   C. wpss 3575   Tr wtr 4752

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-8 1992  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  ax-un 6949

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-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180  df-uni 4437  df-iun 4522  df-tr 4753  df-suc 5729

This theorem is referenced by:  dfon2lem6  31693  dfon2  31697