Users' Mathboxes Mathbox for Jim Kingdon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  pwle2 Unicode version

Theorem pwle2 13349
Description: An exercise related to  N copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.)
Hypothesis
Ref Expression
pwle2.t  |-  T  = 
U_ x  e.  N  ( { x }  X.  1o )
Assertion
Ref Expression
pwle2  |-  ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  ->  N  C_  2o )
Distinct variable group:    x, N
Allowed substitution hints:    T( x)    G( x)

Proof of Theorem pwle2
StepHypRef Expression
1 simplr 520 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  G : T -1-1-> ~P 1o )
2 f1f 5332 . . . . . . . . . . 11  |-  ( G : T -1-1-> ~P 1o  ->  G : T --> ~P 1o )
31, 2syl 14 . . . . . . . . . 10  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  G : T --> ~P 1o )
4 nnon 4527 . . . . . . . . . . . . . 14  |-  ( N  e.  om  ->  N  e.  On )
54ad2antrr 480 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  N  e.  On )
6 simpr 109 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  2o  e.  N )
7 1lt2o 6343 . . . . . . . . . . . . . 14  |-  1o  e.  2o
86, 7jctil 310 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( 1o  e.  2o  /\  2o  e.  N ) )
9 ontr1 4315 . . . . . . . . . . . . 13  |-  ( N  e.  On  ->  (
( 1o  e.  2o  /\  2o  e.  N )  ->  1o  e.  N
) )
105, 8, 9sylc 62 . . . . . . . . . . . 12  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  1o  e.  N )
11 0lt1o 6341 . . . . . . . . . . . 12  |-  (/)  e.  1o
12 opelxpi 4575 . . . . . . . . . . . 12  |-  ( ( 1o  e.  N  /\  (/) 
e.  1o )  ->  <. 1o ,  (/) >.  e.  ( N  X.  1o ) )
1310, 11, 12sylancl 410 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. 1o ,  (/)
>.  e.  ( N  X.  1o ) )
14 pwle2.t . . . . . . . . . . . 12  |-  T  = 
U_ x  e.  N  ( { x }  X.  1o )
15 iunxpconst 4603 . . . . . . . . . . . 12  |-  U_ x  e.  N  ( {
x }  X.  1o )  =  ( N  X.  1o )
1614, 15eqtri 2161 . . . . . . . . . . 11  |-  T  =  ( N  X.  1o )
1713, 16eleqtrrdi 2234 . . . . . . . . . 10  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. 1o ,  (/)
>.  e.  T )
183, 17ffvelrnd 5560 . . . . . . . . 9  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 1o ,  (/)
>. )  e.  ~P 1o )
1918elpwid 3522 . . . . . . . 8  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 1o ,  (/)
>. )  C_  1o )
20 df1o2 6330 . . . . . . . 8  |-  1o  =  { (/) }
2119, 20sseqtrdi 3146 . . . . . . 7  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 1o ,  (/)
>. )  C_  { (/) } )
22 pwtrufal 13348 . . . . . . 7  |-  ( ( G `  <. 1o ,  (/)
>. )  C_  { (/) }  ->  -.  -.  (
( G `  <. 1o ,  (/) >. )  =  (/)  \/  ( G `  <. 1o ,  (/) >. )  =  { (/)
} ) )
2321, 22syl 14 . . . . . 6  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  -.  ( ( G `  <. 1o ,  (/) >. )  =  (/)  \/  ( G `
 <. 1o ,  (/) >.
)  =  { (/) } ) )
24 ioran 742 . . . . . 6  |-  ( -.  ( ( G `  <. 1o ,  (/) >. )  =  (/)  \/  ( G `
 <. 1o ,  (/) >.
)  =  { (/) } )  <->  ( -.  ( G `  <. 1o ,  (/)
>. )  =  (/)  /\  -.  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} ) )
2523, 24sylnib 666 . . . . 5  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( -.  ( G `  <. 1o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} ) )
26 1n0 6333 . . . . . . . . . . 11  |-  1o  =/=  (/)
2726neii 2311 . . . . . . . . . 10  |-  -.  1o  =  (/)
28 1oex 6325 . . . . . . . . . . 11  |-  1o  e.  _V
29 0ex 4059 . . . . . . . . . . 11  |-  (/)  e.  _V
3028, 29opth1 4162 . . . . . . . . . 10  |-  ( <. 1o ,  (/) >.  =  <. (/)
,  (/) >.  ->  1o  =  (/) )
3127, 30mto 652 . . . . . . . . 9  |-  -.  <. 1o ,  (/) >.  =  <. (/)
,  (/) >.
32 0lt2o 6342 . . . . . . . . . . . . . 14  |-  (/)  e.  2o
336, 32jctil 310 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( (/) 
e.  2o  /\  2o  e.  N ) )
34 ontr1 4315 . . . . . . . . . . . . 13  |-  ( N  e.  On  ->  (
( (/)  e.  2o  /\  2o  e.  N )  ->  (/) 
e.  N ) )
355, 33, 34sylc 62 . . . . . . . . . . . 12  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  (/)  e.  N
)
36 opelxpi 4575 . . . . . . . . . . . 12  |-  ( (
(/)  e.  N  /\  (/) 
e.  1o )  ->  <.
(/) ,  (/) >.  e.  ( N  X.  1o ) )
3735, 11, 36sylancl 410 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. (/) ,  (/) >.  e.  ( N  X.  1o ) )
3837, 16eleqtrrdi 2234 . . . . . . . . . 10  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. (/) ,  (/) >.  e.  T )
39 f1veqaeq 5674 . . . . . . . . . 10  |-  ( ( G : T -1-1-> ~P 1o  /\  ( <. 1o ,  (/)
>.  e.  T  /\  <. (/)
,  (/) >.  e.  T
) )  ->  (
( G `  <. 1o ,  (/) >. )  =  ( G `  <. (/) ,  (/) >.
)  ->  <. 1o ,  (/)
>.  =  <. (/) ,  (/) >.
) )
401, 17, 38, 39syl12anc 1215 . . . . . . . . 9  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  (
( G `  <. 1o ,  (/) >. )  =  ( G `  <. (/) ,  (/) >.
)  ->  <. 1o ,  (/)
>.  =  <. (/) ,  (/) >.
) )
4131, 40mtoi 654 . . . . . . . 8  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. (/) ,  (/) >.
) )
4241adantr 274 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 1o ,  (/) >. )  =  ( G `  <. (/) ,  (/) >.
) )
43 simpr 109 . . . . . . . 8  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  -> 
( G `  <. (/)
,  (/) >. )  =  (/) )
4443eqeq2d 2152 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  -> 
( ( G `  <. 1o ,  (/) >. )  =  ( G `  <.
(/) ,  (/) >. )  <->  ( G `  <. 1o ,  (/)
>. )  =  (/) ) )
4542, 44mtbid 662 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 1o ,  (/) >. )  =  (/) )
46 2on0 6327 . . . . . . . . . . . . . 14  |-  2o  =/=  (/)
4746nesymi 2355 . . . . . . . . . . . . 13  |-  -.  (/)  =  2o
4829, 29opth1 4162 . . . . . . . . . . . . 13  |-  ( <. (/)
,  (/) >.  =  <. 2o ,  (/) >.  ->  (/)  =  2o )
4947, 48mto 652 . . . . . . . . . . . 12  |-  -.  <. (/)
,  (/) >.  =  <. 2o ,  (/) >.
50 opelxpi 4575 . . . . . . . . . . . . . . 15  |-  ( ( 2o  e.  N  /\  (/) 
e.  1o )  ->  <. 2o ,  (/) >.  e.  ( N  X.  1o ) )
516, 11, 50sylancl 410 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. 2o ,  (/)
>.  e.  ( N  X.  1o ) )
5251, 16eleqtrrdi 2234 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  <. 2o ,  (/)
>.  e.  T )
53 f1veqaeq 5674 . . . . . . . . . . . . 13  |-  ( ( G : T -1-1-> ~P 1o  /\  ( <. (/) ,  (/) >.  e.  T  /\  <. 2o ,  (/)
>.  e.  T ) )  ->  ( ( G `
 <. (/) ,  (/) >. )  =  ( G `  <. 2o ,  (/) >. )  -> 
<. (/) ,  (/) >.  =  <. 2o ,  (/) >. ) )
541, 38, 52, 53syl12anc 1215 . . . . . . . . . . . 12  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  (
( G `  <. (/)
,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. )  ->  <. (/) ,  (/) >.  =  <. 2o ,  (/) >.
) )
5549, 54mtoi 654 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. (/) ,  (/) >.
)  =  ( G `
 <. 2o ,  (/) >.
) )
5655ad2antrr 480 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  ( G `  <. (/) ,  (/) >.
)  =  ( G `
 <. 2o ,  (/) >.
) )
57 simplr 520 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  ( G `  <. (/) ,  (/) >.
)  =  (/) )
5857eqeq1d 2149 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  (
( G `  <. (/)
,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. )  <->  (/)  =  ( G `
 <. 2o ,  (/) >.
) ) )
5956, 58mtbid 662 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  (/)  =  ( G `  <. 2o ,  (/) >. )
)
60 eqcom 2142 . . . . . . . . 9  |-  ( (/)  =  ( G `  <. 2o ,  (/) >. )  <->  ( G `  <. 2o ,  (/)
>. )  =  (/) )
6159, 60sylnib 666 . . . . . . . 8  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  ( G `  <. 2o ,  (/)
>. )  =  (/) )
62 1onn 6420 . . . . . . . . . . . . . . . . . 18  |-  1o  e.  om
63 peano1 4512 . . . . . . . . . . . . . . . . . 18  |-  (/)  e.  om
64 peano4 4515 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1o  e.  om  /\  (/) 
e.  om )  ->  ( suc  1o  =  suc  (/)  <->  1o  =  (/) ) )
6562, 63, 64mp2an 423 . . . . . . . . . . . . . . . . 17  |-  ( suc 
1o  =  suc  (/)  <->  1o  =  (/) )
6626, 65nemtbir 2398 . . . . . . . . . . . . . . . 16  |-  -.  suc  1o  =  suc  (/)
67 df-2o 6318 . . . . . . . . . . . . . . . . 17  |-  2o  =  suc  1o
68 df-1o 6317 . . . . . . . . . . . . . . . . 17  |-  1o  =  suc  (/)
6967, 68eqeq12i 2154 . . . . . . . . . . . . . . . 16  |-  ( 2o  =  1o  <->  suc  1o  =  suc  (/) )
7066, 69mtbir 661 . . . . . . . . . . . . . . 15  |-  -.  2o  =  1o
7170neir 2312 . . . . . . . . . . . . . 14  |-  2o  =/=  1o
7271nesymi 2355 . . . . . . . . . . . . 13  |-  -.  1o  =  2o
7328, 29opth1 4162 . . . . . . . . . . . . 13  |-  ( <. 1o ,  (/) >.  =  <. 2o ,  (/) >.  ->  1o  =  2o )
7472, 73mto 652 . . . . . . . . . . . 12  |-  -.  <. 1o ,  (/) >.  =  <. 2o ,  (/) >.
75 f1veqaeq 5674 . . . . . . . . . . . . 13  |-  ( ( G : T -1-1-> ~P 1o  /\  ( <. 1o ,  (/)
>.  e.  T  /\  <. 2o ,  (/) >.  e.  T
) )  ->  (
( G `  <. 1o ,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. )  ->  <. 1o ,  (/)
>.  =  <. 2o ,  (/)
>. ) )
761, 17, 52, 75syl12anc 1215 . . . . . . . . . . . 12  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  (
( G `  <. 1o ,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. )  ->  <. 1o ,  (/)
>.  =  <. 2o ,  (/)
>. ) )
7774, 76mtoi 654 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. 2o ,  (/)
>. ) )
7877ad2antrr 480 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. 2o ,  (/)
>. ) )
79 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )
8079eqeq1d 2149 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  (
( G `  <. 1o ,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. )  <->  { (/) }  =  ( G `  <. 2o ,  (/)
>. ) ) )
8178, 80mtbid 662 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  {
(/) }  =  ( G `  <. 2o ,  (/)
>. ) )
82 eqcom 2142 . . . . . . . . 9  |-  ( {
(/) }  =  ( G `  <. 2o ,  (/)
>. )  <->  ( G `  <. 2o ,  (/) >. )  =  { (/) } )
8381, 82sylnib 666 . . . . . . . 8  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} )
8461, 83jca 304 . . . . . . 7  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  ( -.  ( G `  <. 2o ,  (/) >. )  =  (/)  /\ 
-.  ( G `  <. 2o ,  (/) >. )  =  { (/) } ) )
853, 52ffvelrnd 5560 . . . . . . . . . . . 12  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 2o ,  (/)
>. )  e.  ~P 1o )
8685elpwid 3522 . . . . . . . . . . 11  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 2o ,  (/)
>. )  C_  1o )
8786, 20sseqtrdi 3146 . . . . . . . . . 10  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. 2o ,  (/)
>. )  C_  { (/) } )
88 pwtrufal 13348 . . . . . . . . . 10  |-  ( ( G `  <. 2o ,  (/)
>. )  C_  { (/) }  ->  -.  -.  (
( G `  <. 2o ,  (/) >. )  =  (/)  \/  ( G `  <. 2o ,  (/) >. )  =  { (/)
} ) )
8987, 88syl 14 . . . . . . . . 9  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  -.  ( ( G `  <. 2o ,  (/) >. )  =  (/)  \/  ( G `
 <. 2o ,  (/) >.
)  =  { (/) } ) )
90 ioran 742 . . . . . . . . 9  |-  ( -.  ( ( G `  <. 2o ,  (/) >. )  =  (/)  \/  ( G `
 <. 2o ,  (/) >.
)  =  { (/) } )  <->  ( -.  ( G `  <. 2o ,  (/)
>. )  =  (/)  /\  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
9189, 90sylnib 666 . . . . . . . 8  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( -.  ( G `  <. 2o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
9291ad2antrr 480 . . . . . . 7  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  /\  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )  ->  -.  ( -.  ( G `  <. 2o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
9384, 92pm2.65da 651 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 1o ,  (/) >. )  =  { (/)
} )
9445, 93jca 304 . . . . 5  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  (/) )  -> 
( -.  ( G `
 <. 1o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} ) )
9525, 94mtand 655 . . . 4  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. (/) ,  (/) >.
)  =  (/) )
96 eqcom 2142 . . . . . . . . . . 11  |-  ( ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. 2o ,  (/)
>. )  <->  ( G `  <. 2o ,  (/) >. )  =  ( G `  <. 1o ,  (/) >. )
)
9777, 96sylnib 666 . . . . . . . . . 10  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. 2o ,  (/)
>. )  =  ( G `  <. 1o ,  (/)
>. ) )
9897ad2antrr 480 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 2o ,  (/) >. )  =  ( G `  <. 1o ,  (/)
>. ) )
99 simpr 109 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  -> 
( G `  <. 1o ,  (/) >. )  =  (/) )
10099eqeq2d 2152 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  -> 
( ( G `  <. 2o ,  (/) >. )  =  ( G `  <. 1o ,  (/) >. )  <->  ( G `  <. 2o ,  (/)
>. )  =  (/) ) )
10198, 100mtbid 662 . . . . . . . 8  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 2o ,  (/) >. )  =  (/) )
10255ad2antrr 480 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. (/)
,  (/) >. )  =  ( G `  <. 2o ,  (/)
>. ) )
103 eqcom 2142 . . . . . . . . . 10  |-  ( ( G `  <. (/) ,  (/) >.
)  =  ( G `
 <. 2o ,  (/) >.
)  <->  ( G `  <. 2o ,  (/) >. )  =  ( G `  <.
(/) ,  (/) >. )
)
104102, 103sylnib 666 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 2o ,  (/) >. )  =  ( G `  <. (/) ,  (/) >.
) )
105 simplr 520 . . . . . . . . . 10  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  -> 
( G `  <. (/)
,  (/) >. )  =  { (/)
} )
106105eqeq2d 2152 . . . . . . . . 9  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  -> 
( ( G `  <. 2o ,  (/) >. )  =  ( G `  <.
(/) ,  (/) >. )  <->  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
107104, 106mtbid 662 . . . . . . . 8  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( G `  <. 2o ,  (/) >. )  =  { (/)
} )
108101, 107jca 304 . . . . . . 7  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  -> 
( -.  ( G `
 <. 2o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
10991ad2antrr 480 . . . . . . 7  |-  ( ( ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  /\  ( G `
 <. 1o ,  (/) >.
)  =  (/) )  ->  -.  ( -.  ( G `
 <. 2o ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. 2o ,  (/)
>. )  =  { (/)
} ) )
110108, 109pm2.65da 651 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  (/) )
11141adantr 274 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. (/) ,  (/) >.
) )
112 simpr 109 . . . . . . . 8  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  ( G `  <. (/) ,  (/) >. )  =  { (/) } )
113112eqeq2d 2152 . . . . . . 7  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  ( ( G `  <. 1o ,  (/)
>. )  =  ( G `  <. (/) ,  (/) >.
)  <->  ( G `  <. 1o ,  (/) >. )  =  { (/) } ) )
114111, 113mtbid 662 . . . . . 6  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  -.  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} )
115110, 114jca 304 . . . . 5  |-  ( ( ( ( N  e. 
om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  /\  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )  ->  ( -.  ( G `  <. 1o ,  (/)
>. )  =  (/)  /\  -.  ( G `  <. 1o ,  (/)
>. )  =  { (/)
} ) )
11625, 115mtand 655 . . . 4  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( G `  <. (/) ,  (/) >.
)  =  { (/) } )
11795, 116jca 304 . . 3  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( -.  ( G `  <. (/)
,  (/) >. )  =  (/)  /\ 
-.  ( G `  <.
(/) ,  (/) >. )  =  { (/) } ) )
1183, 38ffvelrnd 5560 . . . . . . 7  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. (/) ,  (/) >.
)  e.  ~P 1o )
119118elpwid 3522 . . . . . 6  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. (/) ,  (/) >.
)  C_  1o )
120119, 20sseqtrdi 3146 . . . . 5  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  ( G `  <. (/) ,  (/) >.
)  C_  { (/) } )
121 pwtrufal 13348 . . . . 5  |-  ( ( G `  <. (/) ,  (/) >.
)  C_  { (/) }  ->  -. 
-.  ( ( G `
 <. (/) ,  (/) >. )  =  (/)  \/  ( G `
 <. (/) ,  (/) >. )  =  { (/) } ) )
122120, 121syl 14 . . . 4  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  -.  ( ( G `  <.
(/) ,  (/) >. )  =  (/)  \/  ( G `
 <. (/) ,  (/) >. )  =  { (/) } ) )
123 ioran 742 . . . 4  |-  ( -.  ( ( G `  <.
(/) ,  (/) >. )  =  (/)  \/  ( G `
 <. (/) ,  (/) >. )  =  { (/) } )  <->  ( -.  ( G `  <. (/) ,  (/) >.
)  =  (/)  /\  -.  ( G `  <. (/) ,  (/) >.
)  =  { (/) } ) )
124122, 123sylnib 666 . . 3  |-  ( ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  /\  2o  e.  N )  ->  -.  ( -.  ( G `  <. (/) ,  (/) >. )  =  (/)  /\  -.  ( G `  <. (/) ,  (/) >.
)  =  { (/) } ) )
125117, 124pm2.65da 651 . 2  |-  ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  ->  -.  2o  e.  N )
126 2onn 6421 . . . 4  |-  2o  e.  om
127 nntri1 6396 . . . 4  |-  ( ( N  e.  om  /\  2o  e.  om )  -> 
( N  C_  2o  <->  -.  2o  e.  N ) )
128126, 127mpan2 422 . . 3  |-  ( N  e.  om  ->  ( N  C_  2o  <->  -.  2o  e.  N ) )
129128adantr 274 . 2  |-  ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  ->  ( N  C_  2o 
<->  -.  2o  e.  N
) )
130125, 129mpbird 166 1  |-  ( ( N  e.  om  /\  G : T -1-1-> ~P 1o )  ->  N  C_  2o )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 698    = wceq 1332    e. wcel 1481    C_ wss 3072   (/)c0 3364   ~Pcpw 3511   {csn 3528   <.cop 3531   U_ciun 3817   Oncon0 4289   suc csuc 4291   omcom 4508    X. cxp 4541   -->wf 5123   -1-1->wf1 5124   ` cfv 5127   1oc1o 6310   2oc2o 6311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-iinf 4506
This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-v 2689  df-sbc 2911  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-iun 3819  df-br 3934  df-opab 3994  df-tr 4031  df-id 4219  df-iord 4292  df-on 4294  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fv 5135  df-1o 6317  df-2o 6318
This theorem is referenced by:  pwf1oexmid  13350
  Copyright terms: Public domain W3C validator