Theorem atlrelat1

Description: An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of MaedaMaeda p. 30. ( chpssati , with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011)

	Ref	Expression
Hypotheses	atlrelat1.b	|- B = ( Base ` K )
	atlrelat1.l	|- .<_ = ( le ` K )
	atlrelat1.s	|- .< = ( lt ` K )
	atlrelat1.a	|- A = ( Atoms ` K )
Assertion	atlrelat1	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		atlrelat1.b	|- B = ( Base ` K )
2		atlrelat1.l	|- .<_ = ( le ` K )
3		atlrelat1.s	|- .< = ( lt ` K )
4		atlrelat1.a	|- A = ( Atoms ` K )
5		simp13	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> K e. AtLat )
6		atlpos	|- ( K e. AtLat -> K e. Poset )
7	5 6	syl	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> K e. Poset )
8	1 2 3	pltnle	|- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X .< Y ) -> -. Y .<_ X )
9	8	ex	|- ( ( K e. Poset /\ X e. B /\ Y e. B ) -> ( X .< Y -> -. Y .<_ X ) )
10	7 9	syld3an1	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> -. Y .<_ X ) )
11		iman	|- ( ( p .<_ Y -> p .<_ X ) <-> -. ( p .<_ Y /\ -. p .<_ X ) )
12		ancom	|- ( ( p .<_ Y /\ -. p .<_ X ) <-> ( -. p .<_ X /\ p .<_ Y ) )
13	11 12	xchbinx	|- ( ( p .<_ Y -> p .<_ X ) <-> -. ( -. p .<_ X /\ p .<_ Y ) )
14	13	ralbii	|- ( A. p e. A ( p .<_ Y -> p .<_ X ) <-> A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) )
15	1 2 4	atlatle	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ Y e. B /\ X e. B ) -> ( Y .<_ X <-> A. p e. A ( p .<_ Y -> p .<_ X ) ) )
16	15	3com23	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( Y .<_ X <-> A. p e. A ( p .<_ Y -> p .<_ X ) ) )
17	16	biimprd	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( A. p e. A ( p .<_ Y -> p .<_ X ) -> Y .<_ X ) )
18	14 17	syl5bir	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) -> Y .<_ X ) )
19	18	con3d	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X -> -. A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) ) )
20		dfrex2	|- ( E. p e. A ( -. p .<_ X /\ p .<_ Y ) <-> -. A. p e. A -. ( -. p .<_ X /\ p .<_ Y ) )
21	19 20	syl6ibr	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( -. Y .<_ X -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
22	10 21	syld	|- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )