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

Theorem 4atexlemex2 30553
 Description: Lemma for 4atexlem7 30557. 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 30551 . . 3
121, 2, 3, 4, 5, 6, 7, 8, 94atexlemnclw 30552 . . 3
141, 2, 3, 4, 5, 6, 7, 84atexlemntlpq 30550 . . . . 5
15 id 20 . . . . . . . . . . 11
169, 15syl5eqr 2450 . . . . . . . . . 10
1716adantl 453 . . . . . . . . 9
1814atexlemkl 30539 . . . . . . . . . . . 12
191, 3, 54atexlemqtb 30543 . . . . . . . . . . . 12
201, 3, 54atexlempsb 30542 . . . . . . . . . . . 12
21 eqid 2404 . . . . . . . . . . . . 13
2221, 2, 4latmle1 14460 . . . . . . . . . . . 12
2318, 19, 20, 22syl3anc 1184 . . . . . . . . . . 11
2414atexlemk 30529 . . . . . . . . . . . 12
2514atexlemq 30533 . . . . . . . . . . . 12
2614atexlemt 30535 . . . . . . . . . . . 12
273, 5hlatjcom 29850 . . . . . . . . . . . 12
2824, 25, 26, 27syl3anc 1184 . . . . . . . . . . 11
2923, 28breqtrd 4196 . . . . . . . . . 10
3029adantr 452 . . . . . . . . 9
3117, 30eqbrtrrd 4194 . . . . . . . 8
3214atexlemkc 30540 . . . . . . . . . 10
3314atexlemp 30532 . . . . . . . . . 10
3414atexlempnq 30537 . . . . . . . . . 10
352, 3, 5cvlatexch2 29820 . . . . . . . . . 10
3632, 33, 26, 25, 34, 35syl131anc 1197 . . . . . . . . 9
3736adantr 452 . . . . . . . 8
3831, 37mpd 15 . . . . . . 7
3938ex 424 . . . . . 6
4039necon3bd 2604 . . . . 5
4114, 40mpd 15 . . . 4
43 simpr 448 . . 3
4421, 2, 4latmle2 14461 . . . . . 6
4518, 19, 20, 44syl3anc 1184 . . . . 5
469, 45syl5eqbr 4205 . . . 4
4814atexlems 30534 . . . . 5
491, 2, 3, 54atexlempns 30544 . . . . 5
505, 2, 3cvlsupr2 29826 . . . . 5
5132, 33, 48, 10, 49, 50syl131anc 1197 . . . 4