Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  4atexlemex2 Structured version   Unicode version

Theorem 4atexlemex2 30805
 Description: Lemma for 4atexlem7 30809. Show that when , satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.)
Hypotheses
Ref Expression
4thatlem.ph
4thatlem0.l
4thatlem0.j
4thatlem0.m
4thatlem0.a
4thatlem0.h
4thatlem0.u
4thatlem0.v
4thatlem0.c
Assertion
Ref Expression
4atexlemex2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem 4atexlemex2
StepHypRef Expression
1 4thatlem.ph . . . 4
2 4thatlem0.l . . . 4
3 4thatlem0.j . . . 4
4 4thatlem0.m . . . 4
5 4thatlem0.a . . . 4
6 4thatlem0.h . . . 4
7 4thatlem0.u . . . 4
8 4thatlem0.v . . . 4
9 4thatlem0.c . . . 4
101, 2, 3, 4, 5, 6, 7, 8, 94atexlemc 30803 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 94atexlemnclw 30804 . . 3
141, 2, 3, 4, 5, 6, 7, 84atexlemntlpq 30802 . . . . 5
15 id 20 . . . . . . . . . . 11
169, 15syl5eqr 2481 . . . . . . . . . 10
1716adantl 453 . . . . . . . . 9
1814atexlemkl 30791 . . . . . . . . . . . 12
191, 3, 54atexlemqtb 30795 . . . . . . . . . . . 12
201, 3, 54atexlempsb 30794 . . . . . . . . . . . 12
21 eqid 2435 . . . . . . . . . . . . 13
2221, 2, 4latmle1 14497 . . . . . . . . . . . 12
2318, 19, 20, 22syl3anc 1184 . . . . . . . . . . 11
2414atexlemk 30781 . . . . . . . . . . . 12
2514atexlemq 30785 . . . . . . . . . . . 12
2614atexlemt 30787 . . . . . . . . . . . 12
273, 5hlatjcom 30102 . . . . . . . . . . . 12
2824, 25, 26, 27syl3anc 1184 . . . . . . . . . . 11
2923, 28breqtrd 4228 . . . . . . . . . 10
3029adantr 452 . . . . . . . . 9
3117, 30eqbrtrrd 4226 . . . . . . . 8
3214atexlemkc 30792 . . . . . . . . . 10
3314atexlemp 30784 . . . . . . . . . 10
3414atexlempnq 30789 . . . . . . . . . 10
352, 3, 5cvlatexch2 30072 . . . . . . . . . 10
3632, 33, 26, 25, 34, 35syl131anc 1197 . . . . . . . . 9
3736adantr 452 . . . . . . . 8
3831, 37mpd 15 . . . . . . 7
3938ex 424 . . . . . 6
4039necon3bd 2635 . . . . 5
4114, 40mpd 15 . . . 4
43 simpr 448 . . 3
4421, 2, 4latmle2 14498 . . . . . 6
4518, 19, 20, 44syl3anc 1184 . . . . 5
469, 45syl5eqbr 4237 . . . 4
4814atexlems 30786 . . . . 5
491, 2, 3, 54atexlempns 30796 . . . . 5
505, 2, 3cvlsupr2 30078 . . . . 5
5132, 33, 48, 10, 49, 50syl131anc 1197 . . . 4