Metamath Proof Explorer

Theorem frgrwopreglem5ALT

Description: Alternate direct proof of frgrwopreglem5 , not using frgrwopreglem5a . This proof would be even a little bit shorter than the proof of frgrwopreglem5 without using frgrwopreglem5lem . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 3-Jan-2022) (Proof shortened by AV, 5-Feb-2022) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses frgrwopreg.v 
|- V = ( Vtx ` G )
frgrwopreg.d 
|- D = ( VtxDeg ` G )
frgrwopreg.a 
|- A = { x e. V | ( D ` x ) = K }
frgrwopreg.b 
|- B = ( V \ A )
frgrwopreg.e 
|- E = ( Edg ` G )
Assertion frgrwopreglem5ALT 
|- ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v 
 |-  V = ( Vtx ` G )
2 frgrwopreg.d 
 |-  D = ( VtxDeg ` G )
3 frgrwopreg.a 
 |-  A = { x e. V | ( D ` x ) = K }
4 frgrwopreg.b 
 |-  B = ( V \ A )
5 frgrwopreg.e 
 |-  E = ( Edg ` G )
6 simpllr 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> a =/= x )
7 6 anim1i 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( a =/= x /\ b =/= y ) )
8 1 2 3 4 5 frgrwopreglem4 
 |-  ( G e. FriendGraph -> A. z e. A A. b e. B { z , b } e. E )
9 preq1 
 |-  ( z = a -> { z , b } = { a , b } )
10 9 eleq1d 
 |-  ( z = a -> ( { z , b } e. E <-> { a , b } e. E ) )
11 10 ralbidv 
 |-  ( z = a -> ( A. b e. B { z , b } e. E <-> A. b e. B { a , b } e. E ) )
12 11 cbvralvw 
 |-  ( A. z e. A A. b e. B { z , b } e. E <-> A. a e. A A. b e. B { a , b } e. E )
13 rsp2 
 |-  ( A. a e. A A. b e. B { a , b } e. E -> ( ( a e. A /\ b e. B ) -> { a , b } e. E ) )
14 13 com12 
 |-  ( ( a e. A /\ b e. B ) -> ( A. a e. A A. b e. B { a , b } e. E -> { a , b } e. E ) )
15 14 ad2ant2r 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( A. a e. A A. b e. B { a , b } e. E -> { a , b } e. E ) )
16 12 15 syl5bi 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( A. z e. A A. b e. B { z , b } e. E -> { a , b } e. E ) )
17 16 imp 
 |-  ( ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) /\ A. z e. A A. b e. B { z , b } e. E ) -> { a , b } e. E )
18 prcom 
 |-  { b , x } = { x , b }
19 preq1 
 |-  ( z = x -> { z , b } = { x , b } )
20 19 eleq1d 
 |-  ( z = x -> ( { z , b } e. E <-> { x , b } e. E ) )
21 20 ralbidv 
 |-  ( z = x -> ( A. b e. B { z , b } e. E <-> A. b e. B { x , b } e. E ) )
22 21 cbvralvw 
 |-  ( A. z e. A A. b e. B { z , b } e. E <-> A. x e. A A. b e. B { x , b } e. E )
23 rsp2 
 |-  ( A. x e. A A. b e. B { x , b } e. E -> ( ( x e. A /\ b e. B ) -> { x , b } e. E ) )
24 22 23 sylbi 
 |-  ( A. z e. A A. b e. B { z , b } e. E -> ( ( x e. A /\ b e. B ) -> { x , b } e. E ) )
25 24 com12 
 |-  ( ( x e. A /\ b e. B ) -> ( A. z e. A A. b e. B { z , b } e. E -> { x , b } e. E ) )
26 25 ad2ant2lr 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( A. z e. A A. b e. B { z , b } e. E -> { x , b } e. E ) )
27 26 imp 
 |-  ( ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) /\ A. z e. A A. b e. B { z , b } e. E ) -> { x , b } e. E )
28 18 27 eqeltrid 
 |-  ( ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) /\ A. z e. A A. b e. B { z , b } e. E ) -> { b , x } e. E )
29 17 28 jca 
 |-  ( ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) /\ A. z e. A A. b e. B { z , b } e. E ) -> ( { a , b } e. E /\ { b , x } e. E ) )
30 29 expcom 
 |-  ( A. z e. A A. b e. B { z , b } e. E -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { a , b } e. E /\ { b , x } e. E ) ) )
31 8 30 syl 
 |-  ( G e. FriendGraph -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { a , b } e. E /\ { b , x } e. E ) ) )
32 31 adantr 
 |-  ( ( G e. FriendGraph /\ a =/= x ) -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { a , b } e. E /\ { b , x } e. E ) ) )
33 32 impl 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( { a , b } e. E /\ { b , x } e. E ) )
34 33 adantr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( { a , b } e. E /\ { b , x } e. E ) )
35 preq2 
 |-  ( b = y -> { x , b } = { x , y } )
36 35 eleq1d 
 |-  ( b = y -> ( { x , b } e. E <-> { x , y } e. E ) )
37 20 36 rspc2v 
 |-  ( ( x e. A /\ y e. B ) -> ( A. z e. A A. b e. B { z , b } e. E -> { x , y } e. E ) )
38 37 ad2ant2l 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( A. z e. A A. b e. B { z , b } e. E -> { x , y } e. E ) )
39 38 impcom 
 |-  ( ( A. z e. A A. b e. B { z , b } e. E /\ ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) ) -> { x , y } e. E )
40 prcom 
 |-  { y , a } = { a , y }
41 preq2 
 |-  ( b = y -> { a , b } = { a , y } )
42 41 eleq1d 
 |-  ( b = y -> ( { a , b } e. E <-> { a , y } e. E ) )
43 10 42 rspc2v 
 |-  ( ( a e. A /\ y e. B ) -> ( A. z e. A A. b e. B { z , b } e. E -> { a , y } e. E ) )
44 43 ad2ant2rl 
 |-  ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( A. z e. A A. b e. B { z , b } e. E -> { a , y } e. E ) )
45 44 impcom 
 |-  ( ( A. z e. A A. b e. B { z , b } e. E /\ ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) ) -> { a , y } e. E )
46 40 45 eqeltrid 
 |-  ( ( A. z e. A A. b e. B { z , b } e. E /\ ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) ) -> { y , a } e. E )
47 39 46 jca 
 |-  ( ( A. z e. A A. b e. B { z , b } e. E /\ ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) ) -> ( { x , y } e. E /\ { y , a } e. E ) )
48 47 ex 
 |-  ( A. z e. A A. b e. B { z , b } e. E -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { x , y } e. E /\ { y , a } e. E ) ) )
49 8 48 syl 
 |-  ( G e. FriendGraph -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { x , y } e. E /\ { y , a } e. E ) ) )
50 49 adantr 
 |-  ( ( G e. FriendGraph /\ a =/= x ) -> ( ( ( a e. A /\ x e. A ) /\ ( b e. B /\ y e. B ) ) -> ( { x , y } e. E /\ { y , a } e. E ) ) )
51 50 impl 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( { x , y } e. E /\ { y , a } e. E ) )
52 51 adantr 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( { x , y } e. E /\ { y , a } e. E ) )
53 7 34 52 3jca 
 |-  ( ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) /\ b =/= y ) -> ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )
54 53 ex 
 |-  ( ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) /\ ( b e. B /\ y e. B ) ) -> ( b =/= y -> ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
55 54 reximdvva 
 |-  ( ( ( G e. FriendGraph /\ a =/= x ) /\ ( a e. A /\ x e. A ) ) -> ( E. b e. B E. y e. B b =/= y -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
56 55 exp31 
 |-  ( G e. FriendGraph -> ( a =/= x -> ( ( a e. A /\ x e. A ) -> ( E. b e. B E. y e. B b =/= y -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) ) )
57 56 com24 
 |-  ( G e. FriendGraph -> ( E. b e. B E. y e. B b =/= y -> ( ( a e. A /\ x e. A ) -> ( a =/= x -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) ) )
58 57 imp31 
 |-  ( ( ( G e. FriendGraph /\ E. b e. B E. y e. B b =/= y ) /\ ( a e. A /\ x e. A ) ) -> ( a =/= x -> E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
59 58 reximdvva 
 |-  ( ( G e. FriendGraph /\ E. b e. B E. y e. B b =/= y ) -> ( E. a e. A E. x e. A a =/= x -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
60 59 ex 
 |-  ( G e. FriendGraph -> ( E. b e. B E. y e. B b =/= y -> ( E. a e. A E. x e. A a =/= x -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) )
61 60 com13 
 |-  ( E. a e. A E. x e. A a =/= x -> ( E. b e. B E. y e. B b =/= y -> ( G e. FriendGraph -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) ) )
62 61 imp 
 |-  ( ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) -> ( G e. FriendGraph -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
63 1 2 3 4 frgrwopreglem1 
 |-  ( A e. _V /\ B e. _V )
64 hashgt12el 
 |-  ( ( A e. _V /\ 1 < ( # ` A ) ) -> E. a e. A E. x e. A a =/= x )
65 64 ex 
 |-  ( A e. _V -> ( 1 < ( # ` A ) -> E. a e. A E. x e. A a =/= x ) )
66 hashgt12el 
 |-  ( ( B e. _V /\ 1 < ( # ` B ) ) -> E. b e. B E. y e. B b =/= y )
67 66 ex 
 |-  ( B e. _V -> ( 1 < ( # ` B ) -> E. b e. B E. y e. B b =/= y ) )
68 65 67 im2anan9 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) ) )
69 63 68 ax-mp 
 |-  ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> ( E. a e. A E. x e. A a =/= x /\ E. b e. B E. y e. B b =/= y ) )
70 62 69 syl11 
 |-  ( G e. FriendGraph -> ( ( 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) ) )
71 70 3impib 
 |-  ( ( G e. FriendGraph /\ 1 < ( # ` A ) /\ 1 < ( # ` B ) ) -> E. a e. A E. x e. A E. b e. B E. y e. B ( ( a =/= x /\ b =/= y ) /\ ( { a , b } e. E /\ { b , x } e. E ) /\ ( { x , y } e. E /\ { y , a } e. E ) ) )