Metamath Proof Explorer

Theorem fnwelem

Description: Lemma for fnwe . (Contributed by Mario Carneiro, 10-Mar-2013) (Revised by Mario Carneiro, 18-Nov-2014)

Ref Expression
Hypotheses fnwe.1 
|- T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
fnwe.2 
|- ( ph -> F : A --> B )
fnwe.3 
|- ( ph -> R We B )
fnwe.4 
|- ( ph -> S We A )
fnwe.5 
|- ( ph -> ( F " w ) e. _V )
fnwelem.6 
|- Q = { <. u , v >. | ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) }
fnwelem.7 
|- G = ( z e. A |-> <. ( F ` z ) , z >. )
Assertion fnwelem 
|- ( ph -> T We A )

Proof

Step Hyp Ref Expression
1 fnwe.1 
 |-  T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) }
2 fnwe.2 
 |-  ( ph -> F : A --> B )
3 fnwe.3 
 |-  ( ph -> R We B )
4 fnwe.4 
 |-  ( ph -> S We A )
5 fnwe.5 
 |-  ( ph -> ( F " w ) e. _V )
6 fnwelem.6 
 |-  Q = { <. u , v >. | ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) }
7 fnwelem.7 
 |-  G = ( z e. A |-> <. ( F ` z ) , z >. )
8 ffvelcdm 
 |-  ( ( F : A --> B /\ z e. A ) -> ( F ` z ) e. B )
9 simpr 
 |-  ( ( F : A --> B /\ z e. A ) -> z e. A )
10 8 9 opelxpd 
 |-  ( ( F : A --> B /\ z e. A ) -> <. ( F ` z ) , z >. e. ( B X. A ) )
11 10 7 fmptd 
 |-  ( F : A --> B -> G : A --> ( B X. A ) )
12 frn 
 |-  ( G : A --> ( B X. A ) -> ran G C_ ( B X. A ) )
13 2 11 12 3syl 
 |-  ( ph -> ran G C_ ( B X. A ) )
14 6 wexp 
 |-  ( ( R We B /\ S We A ) -> Q We ( B X. A ) )
15 3 4 14 syl2anc 
 |-  ( ph -> Q We ( B X. A ) )
16 wess 
 |-  ( ran G C_ ( B X. A ) -> ( Q We ( B X. A ) -> Q We ran G ) )
17 13 15 16 sylc 
 |-  ( ph -> Q We ran G )
18 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
19 id 
 |-  ( z = x -> z = x )
20 18 19 opeq12d 
 |-  ( z = x -> <. ( F ` z ) , z >. = <. ( F ` x ) , x >. )
21 opex 
 |-  <. ( F ` x ) , x >. e. _V
22 20 7 21 fvmpt 
 |-  ( x e. A -> ( G ` x ) = <. ( F ` x ) , x >. )
23 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
24 id 
 |-  ( z = y -> z = y )
25 23 24 opeq12d 
 |-  ( z = y -> <. ( F ` z ) , z >. = <. ( F ` y ) , y >. )
26 opex 
 |-  <. ( F ` y ) , y >. e. _V
27 25 7 26 fvmpt 
 |-  ( y e. A -> ( G ` y ) = <. ( F ` y ) , y >. )
28 22 27 eqeqan12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( G ` x ) = ( G ` y ) <-> <. ( F ` x ) , x >. = <. ( F ` y ) , y >. ) )
29 fvex 
 |-  ( F ` x ) e. _V
30 vex 
 |-  x e. _V
31 29 30 opth 
 |-  ( <. ( F ` x ) , x >. = <. ( F ` y ) , y >. <-> ( ( F ` x ) = ( F ` y ) /\ x = y ) )
32 31 simprbi 
 |-  ( <. ( F ` x ) , x >. = <. ( F ` y ) , y >. -> x = y )
33 28 32 biimtrdi 
 |-  ( ( x e. A /\ y e. A ) -> ( ( G ` x ) = ( G ` y ) -> x = y ) )
34 33 rgen2 
 |-  A. x e. A A. y e. A ( ( G ` x ) = ( G ` y ) -> x = y )
35 dff13 
 |-  ( G : A -1-1-> ( B X. A ) <-> ( G : A --> ( B X. A ) /\ A. x e. A A. y e. A ( ( G ` x ) = ( G ` y ) -> x = y ) ) )
36 11 34 35 sylanblrc 
 |-  ( F : A --> B -> G : A -1-1-> ( B X. A ) )
37 f1f1orn 
 |-  ( G : A -1-1-> ( B X. A ) -> G : A -1-1-onto-> ran G )
38 f1ocnv 
 |-  ( G : A -1-1-onto-> ran G -> `' G : ran G -1-1-onto-> A )
39 2 36 37 38 4syl 
 |-  ( ph -> `' G : ran G -1-1-onto-> A )
40 eqid 
 |-  { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) }
41 40 f1oiso2 
 |-  ( `' G : ran G -1-1-onto-> A -> `' G Isom Q , { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } ( ran G , A ) )
42 frel 
 |-  ( G : A --> ( B X. A ) -> Rel G )
43 dfrel2 
 |-  ( Rel G <-> `' `' G = G )
44 42 43 sylib 
 |-  ( G : A --> ( B X. A ) -> `' `' G = G )
45 44 fveq1d 
 |-  ( G : A --> ( B X. A ) -> ( `' `' G ` x ) = ( G ` x ) )
46 44 fveq1d 
 |-  ( G : A --> ( B X. A ) -> ( `' `' G ` y ) = ( G ` y ) )
47 45 46 breq12d 
 |-  ( G : A --> ( B X. A ) -> ( ( `' `' G ` x ) Q ( `' `' G ` y ) <-> ( G ` x ) Q ( G ` y ) ) )
48 11 47 syl 
 |-  ( F : A --> B -> ( ( `' `' G ` x ) Q ( `' `' G ` y ) <-> ( G ` x ) Q ( G ` y ) ) )
49 48 adantr 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( `' `' G ` x ) Q ( `' `' G ` y ) <-> ( G ` x ) Q ( G ` y ) ) )
50 22 27 breqan12d 
 |-  ( ( x e. A /\ y e. A ) -> ( ( G ` x ) Q ( G ` y ) <-> <. ( F ` x ) , x >. Q <. ( F ` y ) , y >. ) )
51 50 adantl 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( G ` x ) Q ( G ` y ) <-> <. ( F ` x ) , x >. Q <. ( F ` y ) , y >. ) )
52 eleq1 
 |-  ( u = <. ( F ` x ) , x >. -> ( u e. ( B X. A ) <-> <. ( F ` x ) , x >. e. ( B X. A ) ) )
53 opelxp 
 |-  ( <. ( F ` x ) , x >. e. ( B X. A ) <-> ( ( F ` x ) e. B /\ x e. A ) )
54 52 53 bitrdi 
 |-  ( u = <. ( F ` x ) , x >. -> ( u e. ( B X. A ) <-> ( ( F ` x ) e. B /\ x e. A ) ) )
55 54 anbi1d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) <-> ( ( ( F ` x ) e. B /\ x e. A ) /\ v e. ( B X. A ) ) ) )
56 29 30 op1std 
 |-  ( u = <. ( F ` x ) , x >. -> ( 1st ` u ) = ( F ` x ) )
57 56 breq1d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( 1st ` u ) R ( 1st ` v ) <-> ( F ` x ) R ( 1st ` v ) ) )
58 56 eqeq1d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( 1st ` u ) = ( 1st ` v ) <-> ( F ` x ) = ( 1st ` v ) ) )
59 29 30 op2ndd 
 |-  ( u = <. ( F ` x ) , x >. -> ( 2nd ` u ) = x )
60 59 breq1d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( 2nd ` u ) S ( 2nd ` v ) <-> x S ( 2nd ` v ) ) )
61 58 60 anbi12d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) <-> ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) ) )
62 57 61 orbi12d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) <-> ( ( F ` x ) R ( 1st ` v ) \/ ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) ) ) )
63 55 62 anbi12d 
 |-  ( u = <. ( F ` x ) , x >. -> ( ( ( u e. ( B X. A ) /\ v e. ( B X. A ) ) /\ ( ( 1st ` u ) R ( 1st ` v ) \/ ( ( 1st ` u ) = ( 1st ` v ) /\ ( 2nd ` u ) S ( 2nd ` v ) ) ) ) <-> ( ( ( ( F ` x ) e. B /\ x e. A ) /\ v e. ( B X. A ) ) /\ ( ( F ` x ) R ( 1st ` v ) \/ ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) ) ) ) )
64 eleq1 
 |-  ( v = <. ( F ` y ) , y >. -> ( v e. ( B X. A ) <-> <. ( F ` y ) , y >. e. ( B X. A ) ) )
65 opelxp 
 |-  ( <. ( F ` y ) , y >. e. ( B X. A ) <-> ( ( F ` y ) e. B /\ y e. A ) )
66 64 65 bitrdi 
 |-  ( v = <. ( F ` y ) , y >. -> ( v e. ( B X. A ) <-> ( ( F ` y ) e. B /\ y e. A ) ) )
67 66 anbi2d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( ( ( F ` x ) e. B /\ x e. A ) /\ v e. ( B X. A ) ) <-> ( ( ( F ` x ) e. B /\ x e. A ) /\ ( ( F ` y ) e. B /\ y e. A ) ) ) )
68 fvex 
 |-  ( F ` y ) e. _V
69 vex 
 |-  y e. _V
70 68 69 op1std 
 |-  ( v = <. ( F ` y ) , y >. -> ( 1st ` v ) = ( F ` y ) )
71 70 breq2d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( F ` x ) R ( 1st ` v ) <-> ( F ` x ) R ( F ` y ) ) )
72 70 eqeq2d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( F ` x ) = ( 1st ` v ) <-> ( F ` x ) = ( F ` y ) ) )
73 68 69 op2ndd 
 |-  ( v = <. ( F ` y ) , y >. -> ( 2nd ` v ) = y )
74 73 breq2d 
 |-  ( v = <. ( F ` y ) , y >. -> ( x S ( 2nd ` v ) <-> x S y ) )
75 72 74 anbi12d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) <-> ( ( F ` x ) = ( F ` y ) /\ x S y ) ) )
76 71 75 orbi12d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( ( F ` x ) R ( 1st ` v ) \/ ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) ) <-> ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) )
77 67 76 anbi12d 
 |-  ( v = <. ( F ` y ) , y >. -> ( ( ( ( ( F ` x ) e. B /\ x e. A ) /\ v e. ( B X. A ) ) /\ ( ( F ` x ) R ( 1st ` v ) \/ ( ( F ` x ) = ( 1st ` v ) /\ x S ( 2nd ` v ) ) ) ) <-> ( ( ( ( F ` x ) e. B /\ x e. A ) /\ ( ( F ` y ) e. B /\ y e. A ) ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) ) )
78 21 26 63 77 6 brab 
 |-  ( <. ( F ` x ) , x >. Q <. ( F ` y ) , y >. <-> ( ( ( ( F ` x ) e. B /\ x e. A ) /\ ( ( F ` y ) e. B /\ y e. A ) ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) )
79 ffvelcdm 
 |-  ( ( F : A --> B /\ x e. A ) -> ( F ` x ) e. B )
80 simpr 
 |-  ( ( F : A --> B /\ x e. A ) -> x e. A )
81 79 80 jca 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( F ` x ) e. B /\ x e. A ) )
82 ffvelcdm 
 |-  ( ( F : A --> B /\ y e. A ) -> ( F ` y ) e. B )
83 simpr 
 |-  ( ( F : A --> B /\ y e. A ) -> y e. A )
84 82 83 jca 
 |-  ( ( F : A --> B /\ y e. A ) -> ( ( F ` y ) e. B /\ y e. A ) )
85 81 84 anim12dan 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( ( F ` x ) e. B /\ x e. A ) /\ ( ( F ` y ) e. B /\ y e. A ) ) )
86 85 biantrurd 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) <-> ( ( ( ( F ` x ) e. B /\ x e. A ) /\ ( ( F ` y ) e. B /\ y e. A ) ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) ) )
87 78 86 bitr4id 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( <. ( F ` x ) , x >. Q <. ( F ` y ) , y >. <-> ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) )
88 49 51 87 3bitrrd 
 |-  ( ( F : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) <-> ( `' `' G ` x ) Q ( `' `' G ` y ) ) )
89 88 pm5.32da 
 |-  ( F : A --> B -> ( ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) <-> ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) ) )
90 89 opabbidv 
 |-  ( F : A --> B -> { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x S y ) ) ) } = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } )
91 1 90 eqtrid 
 |-  ( F : A --> B -> T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } )
92 isoeq3 
 |-  ( T = { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } -> ( `' G Isom Q , T ( ran G , A ) <-> `' G Isom Q , { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } ( ran G , A ) ) )
93 91 92 syl 
 |-  ( F : A --> B -> ( `' G Isom Q , T ( ran G , A ) <-> `' G Isom Q , { <. x , y >. | ( ( x e. A /\ y e. A ) /\ ( `' `' G ` x ) Q ( `' `' G ` y ) ) } ( ran G , A ) ) )
94 41 93 imbitrrid 
 |-  ( F : A --> B -> ( `' G : ran G -1-1-onto-> A -> `' G Isom Q , T ( ran G , A ) ) )
95 2 39 94 sylc 
 |-  ( ph -> `' G Isom Q , T ( ran G , A ) )
96 isocnv 
 |-  ( `' G Isom Q , T ( ran G , A ) -> `' `' G Isom T , Q ( A , ran G ) )
97 95 96 syl 
 |-  ( ph -> `' `' G Isom T , Q ( A , ran G ) )
98 imacnvcnv 
 |-  ( `' `' G " w ) = ( G " w )
99 vex 
 |-  w e. _V
100 xpexg 
 |-  ( ( ( F " w ) e. _V /\ w e. _V ) -> ( ( F " w ) X. w ) e. _V )
101 5 99 100 sylancl 
 |-  ( ph -> ( ( F " w ) X. w ) e. _V )
102 imadmres 
 |-  ( G " dom ( G |` w ) ) = ( G " w )
103 dmres 
 |-  dom ( G |` w ) = ( w i^i dom G )
104 103 elin2 
 |-  ( x e. dom ( G |` w ) <-> ( x e. w /\ x e. dom G ) )
105 simprr 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> x e. dom G )
106 f1dm 
 |-  ( G : A -1-1-> ( B X. A ) -> dom G = A )
107 2 36 106 3syl 
 |-  ( ph -> dom G = A )
108 107 adantr 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> dom G = A )
109 105 108 eleqtrd 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> x e. A )
110 109 22 syl 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> ( G ` x ) = <. ( F ` x ) , x >. )
111 2 ffnd 
 |-  ( ph -> F Fn A )
112 111 adantr 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> F Fn A )
113 dmres 
 |-  dom ( F |` w ) = ( w i^i dom F )
114 inss2 
 |-  ( w i^i dom F ) C_ dom F
115 112 fndmd 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> dom F = A )
116 114 115 sseqtrid 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> ( w i^i dom F ) C_ A )
117 113 116 eqsstrid 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> dom ( F |` w ) C_ A )
118 simprl 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> x e. w )
119 109 115 eleqtrrd 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> x e. dom F )
120 113 elin2 
 |-  ( x e. dom ( F |` w ) <-> ( x e. w /\ x e. dom F ) )
121 118 119 120 sylanbrc 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> x e. dom ( F |` w ) )
122 fnfvima 
 |-  ( ( F Fn A /\ dom ( F |` w ) C_ A /\ x e. dom ( F |` w ) ) -> ( F ` x ) e. ( F " dom ( F |` w ) ) )
123 112 117 121 122 syl3anc 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> ( F ` x ) e. ( F " dom ( F |` w ) ) )
124 imadmres 
 |-  ( F " dom ( F |` w ) ) = ( F " w )
125 123 124 eleqtrdi 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> ( F ` x ) e. ( F " w ) )
126 125 118 opelxpd 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> <. ( F ` x ) , x >. e. ( ( F " w ) X. w ) )
127 110 126 eqeltrd 
 |-  ( ( ph /\ ( x e. w /\ x e. dom G ) ) -> ( G ` x ) e. ( ( F " w ) X. w ) )
128 104 127 sylan2b 
 |-  ( ( ph /\ x e. dom ( G |` w ) ) -> ( G ` x ) e. ( ( F " w ) X. w ) )
129 128 ralrimiva 
 |-  ( ph -> A. x e. dom ( G |` w ) ( G ` x ) e. ( ( F " w ) X. w ) )
130 f1fun 
 |-  ( G : A -1-1-> ( B X. A ) -> Fun G )
131 2 36 130 3syl 
 |-  ( ph -> Fun G )
132 resss 
 |-  ( G |` w ) C_ G
133 dmss 
 |-  ( ( G |` w ) C_ G -> dom ( G |` w ) C_ dom G )
134 132 133 ax-mp 
 |-  dom ( G |` w ) C_ dom G
135 funimass4 
 |-  ( ( Fun G /\ dom ( G |` w ) C_ dom G ) -> ( ( G " dom ( G |` w ) ) C_ ( ( F " w ) X. w ) <-> A. x e. dom ( G |` w ) ( G ` x ) e. ( ( F " w ) X. w ) ) )
136 131 134 135 sylancl 
 |-  ( ph -> ( ( G " dom ( G |` w ) ) C_ ( ( F " w ) X. w ) <-> A. x e. dom ( G |` w ) ( G ` x ) e. ( ( F " w ) X. w ) ) )
137 129 136 mpbird 
 |-  ( ph -> ( G " dom ( G |` w ) ) C_ ( ( F " w ) X. w ) )
138 102 137 eqsstrrid 
 |-  ( ph -> ( G " w ) C_ ( ( F " w ) X. w ) )
139 101 138 ssexd 
 |-  ( ph -> ( G " w ) e. _V )
140 98 139 eqeltrid 
 |-  ( ph -> ( `' `' G " w ) e. _V )
141 140 alrimiv 
 |-  ( ph -> A. w ( `' `' G " w ) e. _V )
142 isowe2 
 |-  ( ( `' `' G Isom T , Q ( A , ran G ) /\ A. w ( `' `' G " w ) e. _V ) -> ( Q We ran G -> T We A ) )
143 97 141 142 syl2anc 
 |-  ( ph -> ( Q We ran G -> T We A ) )
144 17 143 mpd 
 |-  ( ph -> T We A )