MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tskcard Unicode version

Theorem tskcard 8612
Description: An even more direct relationship than r1tskina 8613 to get an inacessible cardinal out of a Tarski's class: the size of any nonempty Tarski's class is an inaccessible cardinal. (Contributed by Mario Carneiro, 9-Jun-2013.)
Assertion
Ref Expression
tskcard  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( card `  T )  e. 
Inacc )

Proof of Theorem tskcard
Dummy variables  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cardeq0 8383 . . . 4  |-  ( T  e.  Tarski  ->  ( ( card `  T )  =  (/)  <->  T  =  (/) ) )
21necon3bid 2602 . . 3  |-  ( T  e.  Tarski  ->  ( ( card `  T )  =/=  (/)  <->  T  =/=  (/) ) )
32biimpar 472 . 2  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( card `  T )  =/=  (/) )
4 eqid 2404 . . . . . 6  |-  ( z  e.  ( cf `  ( aleph `  |^| { x  e.  On  |  ( card `  T )  C_  ( aleph `  x ) } ) )  |->  (har `  ( w `  z
) ) )  =  ( z  e.  ( cf `  ( aleph ` 
|^| { x  e.  On  |  ( card `  T
)  C_  ( aleph `  x ) } ) )  |->  (har `  (
w `  z )
) )
54pwcfsdom 8414 . . . . 5  |-  ( aleph ` 
|^| { x  e.  On  |  ( card `  T
)  C_  ( aleph `  x ) } ) 
~<  ( ( aleph `  |^| { x  e.  On  | 
( card `  T )  C_  ( aleph `  x ) } )  ^m  ( cf `  ( aleph `  |^| { x  e.  On  | 
( card `  T )  C_  ( aleph `  x ) } ) ) )
6 vex 2919 . . . . . . . . . . . . 13  |-  x  e. 
_V
76pwex 4342 . . . . . . . . . . . 12  |-  ~P x  e.  _V
87canth2 7219 . . . . . . . . . . 11  |-  ~P x  ~<  ~P ~P x
9 simpl 444 . . . . . . . . . . . . 13  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  T  e.  Tarski )
10 cardon 7787 . . . . . . . . . . . . . . . . 17  |-  ( card `  T )  e.  On
1110oneli 4648 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( card `  T
)  ->  x  e.  On )
1211adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  x  e.  On )
13 cardsdomelir 7816 . . . . . . . . . . . . . . . 16  |-  ( x  e.  ( card `  T
)  ->  x  ~<  T )
1413adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  x  ~<  T )
15 tskord 8611 . . . . . . . . . . . . . . 15  |-  ( ( T  e.  Tarski  /\  x  e.  On  /\  x  ~<  T )  ->  x  e.  T )
169, 12, 14, 15syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  x  e.  T )
17 tskpw 8584 . . . . . . . . . . . . . . 15  |-  ( ( T  e.  Tarski  /\  x  e.  T )  ->  ~P x  e.  T )
18 tskpwss 8583 . . . . . . . . . . . . . . 15  |-  ( ( T  e.  Tarski  /\  ~P x  e.  T )  ->  ~P ~P x  C_  T )
1917, 18syldan 457 . . . . . . . . . . . . . 14  |-  ( ( T  e.  Tarski  /\  x  e.  T )  ->  ~P ~P x  C_  T )
2016, 19syldan 457 . . . . . . . . . . . . 13  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  ~P ~P x  C_  T )
21 ssdomg 7112 . . . . . . . . . . . . 13  |-  ( T  e.  Tarski  ->  ( ~P ~P x  C_  T  ->  ~P ~P x  ~<_  T )
)
229, 20, 21sylc 58 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  ~P ~P x  ~<_  T )
23 cardidg 8379 . . . . . . . . . . . . . 14  |-  ( T  e.  Tarski  ->  ( card `  T
)  ~~  T )
2423ensymd 7117 . . . . . . . . . . . . 13  |-  ( T  e.  Tarski  ->  T  ~~  ( card `  T ) )
2524adantr 452 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  T  ~~  ( card `  T
) )
26 domentr 7125 . . . . . . . . . . . 12  |-  ( ( ~P ~P x  ~<_  T  /\  T  ~~  ( card `  T ) )  ->  ~P ~P x  ~<_  ( card `  T )
)
2722, 25, 26syl2anc 643 . . . . . . . . . . 11  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  ~P ~P x  ~<_  ( card `  T ) )
28 sdomdomtr 7199 . . . . . . . . . . 11  |-  ( ( ~P x  ~<  ~P ~P x  /\  ~P ~P x  ~<_  ( card `  T )
)  ->  ~P x  ~<  ( card `  T
) )
298, 27, 28sylancr 645 . . . . . . . . . 10  |-  ( ( T  e.  Tarski  /\  x  e.  ( card `  T
) )  ->  ~P x  ~<  ( card `  T
) )
3029ralrimiva 2749 . . . . . . . . 9  |-  ( T  e.  Tarski  ->  A. x  e.  (
card `  T ) ~P x  ~<  ( card `  T ) )
3130adantr 452 . . . . . . . 8  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  A. x  e.  ( card `  T
) ~P x  ~<  (
card `  T )
)
32 inawinalem 8520 . . . . . . . . . 10  |-  ( (
card `  T )  e.  On  ->  ( A. x  e.  ( card `  T ) ~P x  ~<  ( card `  T
)  ->  A. x  e.  ( card `  T
) E. y  e.  ( card `  T
) x  ~<  y
) )
3310, 32ax-mp 8 . . . . . . . . 9  |-  ( A. x  e.  ( card `  T ) ~P x  ~<  ( card `  T
)  ->  A. x  e.  ( card `  T
) E. y  e.  ( card `  T
) x  ~<  y
)
34 winainflem 8524 . . . . . . . . . 10  |-  ( ( ( card `  T
)  =/=  (/)  /\  ( card `  T )  e.  On  /\  A. x  e.  ( card `  T
) E. y  e.  ( card `  T
) x  ~<  y
)  ->  om  C_  ( card `  T ) )
3510, 34mp3an2 1267 . . . . . . . . 9  |-  ( ( ( card `  T
)  =/=  (/)  /\  A. x  e.  ( card `  T ) E. y  e.  ( card `  T
) x  ~<  y
)  ->  om  C_  ( card `  T ) )
3633, 35sylan2 461 . . . . . . . 8  |-  ( ( ( card `  T
)  =/=  (/)  /\  A. x  e.  ( card `  T ) ~P x  ~<  ( card `  T
) )  ->  om  C_  ( card `  T ) )
373, 31, 36syl2anc 643 . . . . . . 7  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  om  C_  ( card `  T ) )
38 cardidm 7802 . . . . . . 7  |-  ( card `  ( card `  T
) )  =  (
card `  T )
39 cardaleph 7926 . . . . . . 7  |-  ( ( om  C_  ( card `  T )  /\  ( card `  ( card `  T
) )  =  (
card `  T )
)  ->  ( card `  T )  =  (
aleph `  |^| { x  e.  On  |  ( card `  T )  C_  ( aleph `  x ) } ) )
4037, 38, 39sylancl 644 . . . . . 6  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( card `  T )  =  ( aleph `  |^| { x  e.  On  |  ( card `  T )  C_  ( aleph `  x ) } ) )
4140fveq2d 5691 . . . . . . 7  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( cf `  ( card `  T
) )  =  ( cf `  ( aleph ` 
|^| { x  e.  On  |  ( card `  T
)  C_  ( aleph `  x ) } ) ) )
4240, 41oveq12d 6058 . . . . . 6  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) )  =  ( (
aleph `  |^| { x  e.  On  |  ( card `  T )  C_  ( aleph `  x ) } )  ^m  ( cf `  ( aleph `  |^| { x  e.  On  |  ( card `  T )  C_  ( aleph `  x ) } ) ) ) )
4340, 42breq12d 4185 . . . . 5  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  (
( card `  T )  ~<  ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  <->  ( aleph ` 
|^| { x  e.  On  |  ( card `  T
)  C_  ( aleph `  x ) } ) 
~<  ( ( aleph `  |^| { x  e.  On  | 
( card `  T )  C_  ( aleph `  x ) } )  ^m  ( cf `  ( aleph `  |^| { x  e.  On  | 
( card `  T )  C_  ( aleph `  x ) } ) ) ) ) )
445, 43mpbiri 225 . . . 4  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( card `  T )  ~< 
( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) ) )
45 simp1 957 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  T  e.  Tarski )
46 simp3 959 . . . . . . . . . . . . 13  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  x  e.  ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) ) )
47 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( card `  T )  e.  _V
48 fvex 5701 . . . . . . . . . . . . . . . 16  |-  ( cf `  ( card `  T
) )  e.  _V
4947, 48elmap 7001 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  <->  x :
( cf `  ( card `  T ) ) --> ( card `  T
) )
50 fssxp 5561 . . . . . . . . . . . . . . 15  |-  ( x : ( cf `  ( card `  T ) ) --> ( card `  T
)  ->  x  C_  (
( cf `  ( card `  T ) )  X.  ( card `  T
) ) )
5149, 50sylbi 188 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  ->  x  C_  ( ( cf `  ( card `  T
) )  X.  ( card `  T ) ) )
5216ex 424 . . . . . . . . . . . . . . . 16  |-  ( T  e.  Tarski  ->  ( x  e.  ( card `  T
)  ->  x  e.  T ) )
5352ssrdv 3314 . . . . . . . . . . . . . . 15  |-  ( T  e.  Tarski  ->  ( card `  T
)  C_  T )
54 cfle 8090 . . . . . . . . . . . . . . . . 17  |-  ( cf `  ( card `  T
) )  C_  ( card `  T )
55 sstr 3316 . . . . . . . . . . . . . . . . 17  |-  ( ( ( cf `  ( card `  T ) ) 
C_  ( card `  T
)  /\  ( card `  T )  C_  T
)  ->  ( cf `  ( card `  T
) )  C_  T
)
5654, 55mpan 652 . . . . . . . . . . . . . . . 16  |-  ( (
card `  T )  C_  T  ->  ( cf `  ( card `  T
) )  C_  T
)
57 tskxpss 8603 . . . . . . . . . . . . . . . . . 18  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  C_  T  /\  ( card `  T
)  C_  T )  ->  ( ( cf `  ( card `  T ) )  X.  ( card `  T
) )  C_  T
)
58573exp 1152 . . . . . . . . . . . . . . . . 17  |-  ( T  e.  Tarski  ->  ( ( cf `  ( card `  T
) )  C_  T  ->  ( ( card `  T
)  C_  T  ->  ( ( cf `  ( card `  T ) )  X.  ( card `  T
) )  C_  T
) ) )
5958com23 74 . . . . . . . . . . . . . . . 16  |-  ( T  e.  Tarski  ->  ( ( card `  T )  C_  T  ->  ( ( cf `  ( card `  T ) ) 
C_  T  ->  (
( cf `  ( card `  T ) )  X.  ( card `  T
) )  C_  T
) ) )
6056, 59mpdi 40 . . . . . . . . . . . . . . 15  |-  ( T  e.  Tarski  ->  ( ( card `  T )  C_  T  ->  ( ( cf `  ( card `  T ) )  X.  ( card `  T
) )  C_  T
) )
6153, 60mpd 15 . . . . . . . . . . . . . 14  |-  ( T  e.  Tarski  ->  ( ( cf `  ( card `  T
) )  X.  ( card `  T ) ) 
C_  T )
62 sstr2 3315 . . . . . . . . . . . . . 14  |-  ( x 
C_  ( ( cf `  ( card `  T
) )  X.  ( card `  T ) )  ->  ( ( ( cf `  ( card `  T ) )  X.  ( card `  T
) )  C_  T  ->  x  C_  T )
)
6351, 61, 62syl2im 36 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  -> 
( T  e.  Tarski  ->  x  C_  T ) )
6446, 45, 63sylc 58 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  x  C_  T )
65 simp2 958 . . . . . . . . . . . . 13  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  ( cf `  ( card `  T
) )  e.  (
card `  T )
)
66 ffn 5550 . . . . . . . . . . . . . . . . 17  |-  ( x : ( cf `  ( card `  T ) ) --> ( card `  T
)  ->  x  Fn  ( cf `  ( card `  T ) ) )
67 fndmeng 7142 . . . . . . . . . . . . . . . . 17  |-  ( ( x  Fn  ( cf `  ( card `  T
) )  /\  ( cf `  ( card `  T
) )  e.  _V )  ->  ( cf `  ( card `  T ) ) 
~~  x )
6866, 48, 67sylancl 644 . . . . . . . . . . . . . . . 16  |-  ( x : ( cf `  ( card `  T ) ) --> ( card `  T
)  ->  ( cf `  ( card `  T
) )  ~~  x
)
6949, 68sylbi 188 . . . . . . . . . . . . . . 15  |-  ( x  e.  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  -> 
( cf `  ( card `  T ) ) 
~~  x )
7069ensymd 7117 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  ->  x  ~~  ( cf `  ( card `  T ) ) )
71 cardsdomelir 7816 . . . . . . . . . . . . . 14  |-  ( ( cf `  ( card `  T ) )  e.  ( card `  T
)  ->  ( cf `  ( card `  T
) )  ~<  T )
72 ensdomtr 7202 . . . . . . . . . . . . . 14  |-  ( ( x  ~~  ( cf `  ( card `  T
) )  /\  ( cf `  ( card `  T
) )  ~<  T )  ->  x  ~<  T )
7370, 71, 72syl2an 464 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( (
card `  T )  ^m  ( cf `  ( card `  T ) ) )  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  x  ~<  T )
7446, 65, 73syl2anc 643 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  x  ~<  T )
75 tskssel 8588 . . . . . . . . . . . 12  |-  ( ( T  e.  Tarski  /\  x  C_  T  /\  x  ~<  T )  ->  x  e.  T )
7645, 64, 74, 75syl3anc 1184 . . . . . . . . . . 11  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )  /\  x  e.  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) ) )  ->  x  e.  T )
77763expia 1155 . . . . . . . . . 10  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  ( x  e.  ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  ->  x  e.  T )
)
7877ssrdv 3314 . . . . . . . . 9  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  ( ( card `  T )  ^m  ( cf `  ( card `  T ) ) ) 
C_  T )
79 ssdomg 7112 . . . . . . . . . 10  |-  ( T  e.  Tarski  ->  ( ( (
card `  T )  ^m  ( cf `  ( card `  T ) ) )  C_  T  ->  ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  ~<_  T ) )
8079imp 419 . . . . . . . . 9  |-  ( ( T  e.  Tarski  /\  (
( card `  T )  ^m  ( cf `  ( card `  T ) ) )  C_  T )  ->  ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  ~<_  T )
8178, 80syldan 457 . . . . . . . 8  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  ( ( card `  T )  ^m  ( cf `  ( card `  T ) ) )  ~<_  T )
8224adantr 452 . . . . . . . 8  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  T  ~~  ( card `  T )
)
83 domentr 7125 . . . . . . . 8  |-  ( ( ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  ~<_  T  /\  T  ~~  ( card `  T ) )  ->  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) )  ~<_  (
card `  T )
)
8481, 82, 83syl2anc 643 . . . . . . 7  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  ( ( card `  T )  ^m  ( cf `  ( card `  T ) ) )  ~<_  ( card `  T
) )
85 domnsym 7192 . . . . . . 7  |-  ( ( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) )  ~<_  (
card `  T )  ->  -.  ( card `  T
)  ~<  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) ) )
8684, 85syl 16 . . . . . 6  |-  ( ( T  e.  Tarski  /\  ( cf `  ( card `  T
) )  e.  (
card `  T )
)  ->  -.  ( card `  T )  ~< 
( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) ) )
8786ex 424 . . . . 5  |-  ( T  e.  Tarski  ->  ( ( cf `  ( card `  T
) )  e.  (
card `  T )  ->  -.  ( card `  T
)  ~<  ( ( card `  T )  ^m  ( cf `  ( card `  T
) ) ) ) )
8887adantr 452 . . . 4  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  (
( cf `  ( card `  T ) )  e.  ( card `  T
)  ->  -.  ( card `  T )  ~< 
( ( card `  T
)  ^m  ( cf `  ( card `  T
) ) ) ) )
8944, 88mt2d 111 . . 3  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  -.  ( cf `  ( card `  T ) )  e.  ( card `  T
) )
90 cfon 8091 . . . . . 6  |-  ( cf `  ( card `  T
) )  e.  On
9190, 10onsseli 4655 . . . . 5  |-  ( ( cf `  ( card `  T ) )  C_  ( card `  T )  <->  ( ( cf `  ( card `  T ) )  e.  ( card `  T
)  \/  ( cf `  ( card `  T
) )  =  (
card `  T )
) )
9254, 91mpbi 200 . . . 4  |-  ( ( cf `  ( card `  T ) )  e.  ( card `  T
)  \/  ( cf `  ( card `  T
) )  =  (
card `  T )
)
9392ori 365 . . 3  |-  ( -.  ( cf `  ( card `  T ) )  e.  ( card `  T
)  ->  ( cf `  ( card `  T
) )  =  (
card `  T )
)
9489, 93syl 16 . 2  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( cf `  ( card `  T
) )  =  (
card `  T )
)
95 elina 8518 . 2  |-  ( (
card `  T )  e.  Inacc 
<->  ( ( card `  T
)  =/=  (/)  /\  ( cf `  ( card `  T
) )  =  (
card `  T )  /\  A. x  e.  (
card `  T ) ~P x  ~<  ( card `  T ) ) )
963, 94, 31, 95syl3anbrc 1138 1  |-  ( ( T  e.  Tarski  /\  T  =/=  (/) )  ->  ( card `  T )  e. 
Inacc )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358    /\ wa 359    /\ w3a 936    = wceq 1649    e. wcel 1721    =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916    C_ wss 3280   (/)c0 3588   ~Pcpw 3759   |^|cint 4010   class class class wbr 4172    e. cmpt 4226   Oncon0 4541   omcom 4804    X. cxp 4835    Fn wfn 5408   -->wf 5409   ` cfv 5413  (class class class)co 6040    ^m cmap 6977    ~~ cen 7065    ~<_ cdom 7066    ~< csdm 7067  harchar 7480   cardccrd 7778   alephcale 7779   cfccf 7780   Inacccina 8514   Tarskictsk 8579
This theorem is referenced by:  r1tskina  8613  tskuni  8614  inaprc  8667
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-ac2 8299
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-smo 6567  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-har 7482  df-r1 7646  df-card 7782  df-aleph 7783  df-cf 7784  df-acn 7785  df-ac 7953  df-ina 8516  df-tsk 8580
  Copyright terms: Public domain W3C validator