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

Theorem domtriomlem 8715
Description: Lemma for domtriom 8716. (Contributed by Mario Carneiro, 9-Feb-2013.)
Hypotheses
Ref Expression
domtriomlem.1  |-  A  e. 
_V
domtriomlem.2  |-  B  =  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }
domtriomlem.3  |-  C  =  ( n  e.  om  |->  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
) )
Assertion
Ref Expression
domtriomlem  |-  ( -.  A  e.  Fin  ->  om  ~<_  A )
Distinct variable groups:    A, b, n, y    B, b    C, k, n    k, b    y,
b
Allowed substitution hints:    A( k)    B( y, k, n)    C( y,
b)

Proof of Theorem domtriomlem
Dummy variables  c  m  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 domtriomlem.2 . . . . 5  |-  B  =  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }
2 domtriomlem.1 . . . . . . 7  |-  A  e. 
_V
32pwex 4576 . . . . . 6  |-  ~P A  e.  _V
4 simpl 457 . . . . . . . 8  |-  ( ( y  C_  A  /\  y  ~~  ~P n )  ->  y  C_  A
)
54ss2abi 3525 . . . . . . 7  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  C_  { y  |  y  C_  A }
6 df-pw 3963 . . . . . . 7  |-  ~P A  =  { y  |  y 
C_  A }
75, 6sseqtr4i 3490 . . . . . 6  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  C_  ~P A
83, 7ssexi 4538 . . . . 5  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  e.  _V
91, 8eqeltri 2535 . . . 4  |-  B  e. 
_V
10 omex 7953 . . . . 5  |-  om  e.  _V
1110enref 7445 . . . 4  |-  om  ~~  om
129, 11axcc3 8711 . . 3  |-  E. b
( b  Fn  om  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )
13 nfv 1674 . . . . . . . 8  |-  F/ n  -.  A  e.  Fin
14 nfra1 2806 . . . . . . . 8  |-  F/ n A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B )
1513, 14nfan 1863 . . . . . . 7  |-  F/ n
( -.  A  e. 
Fin  /\  A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) )
16 nnfi 7607 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  n  e.  Fin )
17 pwfi 7710 . . . . . . . . . . . . . 14  |-  ( n  e.  Fin  <->  ~P n  e.  Fin )
1816, 17sylib 196 . . . . . . . . . . . . 13  |-  ( n  e.  om  ->  ~P n  e.  Fin )
19 ficardom 8235 . . . . . . . . . . . . 13  |-  ( ~P n  e.  Fin  ->  (
card `  ~P n
)  e.  om )
20 isinf 7630 . . . . . . . . . . . . . 14  |-  ( -.  A  e.  Fin  ->  A. m  e.  om  E. y ( y  C_  A  /\  y  ~~  m
) )
21 breq2 4397 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( card `  ~P n )  ->  (
y  ~~  m  <->  y  ~~  ( card `  ~P n
) ) )
2221anbi2d 703 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( card `  ~P n )  ->  (
( y  C_  A  /\  y  ~~  m )  <-> 
( y  C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2322exbidv 1681 . . . . . . . . . . . . . . 15  |-  ( m  =  ( card `  ~P n )  ->  ( E. y ( y  C_  A  /\  y  ~~  m
)  <->  E. y ( y 
C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2423rspcv 3168 . . . . . . . . . . . . . 14  |-  ( (
card `  ~P n
)  e.  om  ->  ( A. m  e.  om  E. y ( y  C_  A  /\  y  ~~  m
)  ->  E. y
( y  C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2520, 24syl5 32 . . . . . . . . . . . . 13  |-  ( (
card `  ~P n
)  e.  om  ->  ( -.  A  e.  Fin  ->  E. y ( y 
C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2618, 19, 253syl 20 . . . . . . . . . . . 12  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  E. y ( y 
C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
27 finnum 8222 . . . . . . . . . . . . . . 15  |-  ( ~P n  e.  Fin  ->  ~P n  e.  dom  card )
28 cardid2 8227 . . . . . . . . . . . . . . 15  |-  ( ~P n  e.  dom  card  -> 
( card `  ~P n
)  ~~  ~P n
)
29 entr 7464 . . . . . . . . . . . . . . . 16  |-  ( ( y  ~~  ( card `  ~P n )  /\  ( card `  ~P n
)  ~~  ~P n
)  ->  y  ~~  ~P n )
3029expcom 435 . . . . . . . . . . . . . . 15  |-  ( (
card `  ~P n
)  ~~  ~P n  ->  ( y  ~~  ( card `  ~P n )  ->  y  ~~  ~P n ) )
3118, 27, 28, 304syl 21 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  (
y  ~~  ( card `  ~P n )  -> 
y  ~~  ~P n
) )
3231anim2d 565 . . . . . . . . . . . . 13  |-  ( n  e.  om  ->  (
( y  C_  A  /\  y  ~~  ( card `  ~P n ) )  ->  ( y  C_  A  /\  y  ~~  ~P n ) ) )
3332eximdv 1677 . . . . . . . . . . . 12  |-  ( n  e.  om  ->  ( E. y ( y  C_  A  /\  y  ~~  ( card `  ~P n ) )  ->  E. y
( y  C_  A  /\  y  ~~  ~P n
) ) )
3426, 33syld 44 . . . . . . . . . . 11  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  E. y ( y 
C_  A  /\  y  ~~  ~P n ) ) )
351neeq1i 2733 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  =/=  (/) )
36 abn0 3757 . . . . . . . . . . . 12  |-  ( { y  |  ( y 
C_  A  /\  y  ~~  ~P n ) }  =/=  (/)  <->  E. y ( y 
C_  A  /\  y  ~~  ~P n ) )
3735, 36bitri 249 . . . . . . . . . . 11  |-  ( B  =/=  (/)  <->  E. y ( y 
C_  A  /\  y  ~~  ~P n ) )
3834, 37syl6ibr 227 . . . . . . . . . 10  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  B  =/=  (/) ) )
3938com12 31 . . . . . . . . 9  |-  ( -.  A  e.  Fin  ->  ( n  e.  om  ->  B  =/=  (/) ) )
4039adantr 465 . . . . . . . 8  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  -> 
( n  e.  om  ->  B  =/=  (/) ) )
41 rsp 2887 . . . . . . . . 9  |-  ( A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
)  ->  ( n  e.  om  ->  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) ) )
4241adantl 466 . . . . . . . 8  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  -> 
( n  e.  om  ->  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) ) )
4340, 42mpdd 40 . . . . . . 7  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  -> 
( n  e.  om  ->  ( b `  n
)  e.  B ) )
4415, 43ralrimi 2818 . . . . . 6  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  ->  A. n  e.  om  ( b `  n
)  e.  B )
45443adant2 1007 . . . . 5  |-  ( ( -.  A  e.  Fin  /\  b  Fn  om  /\  A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) )  ->  A. n  e.  om  ( b `  n )  e.  B
)
46453expib 1191 . . . 4  |-  ( -.  A  e.  Fin  ->  ( ( b  Fn  om  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  ->  A. n  e.  om  ( b `  n
)  e.  B ) )
4746eximdv 1677 . . 3  |-  ( -.  A  e.  Fin  ->  ( E. b ( b  Fn  om  /\  A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) )  ->  E. b A. n  e.  om  ( b `  n
)  e.  B ) )
4812, 47mpi 17 . 2  |-  ( -.  A  e.  Fin  ->  E. b A. n  e. 
om  ( b `  n )  e.  B
)
49 axcc2 8710 . . . . 5  |-  E. c
( c  Fn  om  /\ 
A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )
50 simp2 989 . . . . . . . 8  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
c  Fn  om )
51 nfra1 2806 . . . . . . . . . . 11  |-  F/ n A. n  e.  om  ( b `  n
)  e.  B
52 nfra1 2806 . . . . . . . . . . 11  |-  F/ n A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) )
5351, 52nfan 1863 . . . . . . . . . 10  |-  F/ n
( A. n  e. 
om  ( b `  n )  e.  B  /\  A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )
54 fvex 5802 . . . . . . . . . . . . . . . 16  |-  ( b `
 n )  e. 
_V
55 sseq1 3478 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( b `  n )  ->  (
y  C_  A  <->  ( b `  n )  C_  A
) )
56 breq1 4396 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( b `  n )  ->  (
y  ~~  ~P n  <->  ( b `  n ) 
~~  ~P n ) )
5755, 56anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( b `  n )  ->  (
( y  C_  A  /\  y  ~~  ~P n
)  <->  ( ( b `
 n )  C_  A  /\  ( b `  n )  ~~  ~P n ) ) )
5854, 57, 1elab2 3209 . . . . . . . . . . . . . . 15  |-  ( ( b `  n )  e.  B  <->  ( (
b `  n )  C_  A  /\  ( b `
 n )  ~~  ~P n ) )
5958simprbi 464 . . . . . . . . . . . . . 14  |-  ( ( b `  n )  e.  B  ->  (
b `  n )  ~~  ~P n )
6059ralimi 2814 . . . . . . . . . . . . 13  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  A. n  e.  om  ( b `  n )  ~~  ~P n )
61 fveq2 5792 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  (
b `  n )  =  ( b `  k ) )
62 pweq 3964 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  ~P n  =  ~P k
)
6361, 62breq12d 4406 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  (
( b `  n
)  ~~  ~P n  <->  ( b `  k ) 
~~  ~P k ) )
6463cbvralv 3046 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  om  (
b `  n )  ~~  ~P n  <->  A. k  e.  om  ( b `  k )  ~~  ~P k )
65 peano2 6599 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  om  ->  suc  n  e.  om )
66 omelon 7956 . . . . . . . . . . . . . . . . . . 19  |-  om  e.  On
6766onelssi 4928 . . . . . . . . . . . . . . . . . 18  |-  ( suc  n  e.  om  ->  suc  n  C_  om )
68 ssralv 3517 . . . . . . . . . . . . . . . . . 18  |-  ( suc  n  C_  om  ->  ( A. k  e.  om  ( b `  k
)  ~~  ~P k  ->  A. k  e.  suc  n ( b `  k )  ~~  ~P k ) )
6965, 67, 683syl 20 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  om  ->  ( A. k  e.  om  ( b `  k
)  ~~  ~P k  ->  A. k  e.  suc  n ( b `  k )  ~~  ~P k ) )
70 pwsdompw 8477 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  om  /\  A. k  e.  suc  n
( b `  k
)  ~~  ~P k
)  ->  U_ k  e.  n  ( b `  k )  ~<  (
b `  n )
)
7170ex 434 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  om  ->  ( A. k  e.  suc  n ( b `  k )  ~~  ~P k  ->  U_ k  e.  n  ( b `  k
)  ~<  ( b `  n ) ) )
7269, 71syld 44 . . . . . . . . . . . . . . . 16  |-  ( n  e.  om  ->  ( A. k  e.  om  ( b `  k
)  ~~  ~P k  ->  U_ k  e.  n  ( b `  k
)  ~<  ( b `  n ) ) )
73 sdomdif 7562 . . . . . . . . . . . . . . . 16  |-  ( U_ k  e.  n  (
b `  k )  ~<  ( b `  n
)  ->  ( (
b `  n )  \  U_ k  e.  n  ( b `  k
) )  =/=  (/) )
7472, 73syl6 33 . . . . . . . . . . . . . . 15  |-  ( n  e.  om  ->  ( A. k  e.  om  ( b `  k
)  ~~  ~P k  ->  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
)  =/=  (/) ) )
7564, 74syl5bi 217 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  ( A. n  e.  om  ( b `  n
)  ~~  ~P n  ->  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
)  =/=  (/) ) )
76 difss 3584 . . . . . . . . . . . . . . . . 17  |-  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) )  C_  (
b `  n )
7754, 76ssexi 4538 . . . . . . . . . . . . . . . 16  |-  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) )  e.  _V
78 domtriomlem.3 . . . . . . . . . . . . . . . . 17  |-  C  =  ( n  e.  om  |->  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
) )
7978fvmpt2 5883 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  om  /\  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
)  e.  _V )  ->  ( C `  n
)  =  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) ) )
8077, 79mpan2 671 . . . . . . . . . . . . . . 15  |-  ( n  e.  om  ->  ( C `  n )  =  ( ( b `
 n )  \  U_ k  e.  n  ( b `  k
) ) )
8180neeq1d 2725 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  (
( C `  n
)  =/=  (/)  <->  ( (
b `  n )  \  U_ k  e.  n  ( b `  k
) )  =/=  (/) ) )
8275, 81sylibrd 234 . . . . . . . . . . . . 13  |-  ( n  e.  om  ->  ( A. n  e.  om  ( b `  n
)  ~~  ~P n  ->  ( C `  n
)  =/=  (/) ) )
8360, 82syl5com 30 . . . . . . . . . . . 12  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( n  e.  om  ->  ( C `  n )  =/=  (/) ) )
8483adantr 465 . . . . . . . . . . 11  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
( n  e.  om  ->  ( C `  n
)  =/=  (/) ) )
85 rsp 2887 . . . . . . . . . . . 12  |-  ( A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) )  ->  (
n  e.  om  ->  ( ( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) ) )
8685adantl 466 . . . . . . . . . . 11  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
( n  e.  om  ->  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) ) )
8784, 86mpdd 40 . . . . . . . . . 10  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
( n  e.  om  ->  ( c `  n
)  e.  ( C `
 n ) ) )
8853, 87ralrimi 2818 . . . . . . . . 9  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  ->  A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) )
89883adant2 1007 . . . . . . . 8  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  ->  A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) )
9050, 89jca 532 . . . . . . 7  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
( c  Fn  om  /\ 
A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) ) )
91903expib 1191 . . . . . 6  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( ( c  Fn  om  /\  A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )  -> 
( c  Fn  om  /\ 
A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) ) ) )
9291eximdv 1677 . . . . 5  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( E. c ( c  Fn 
om  /\  A. n  e.  om  ( ( C `
 n )  =/=  (/)  ->  ( c `  n )  e.  ( C `  n ) ) )  ->  E. c
( c  Fn  om  /\ 
A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) ) ) )
9349, 92mpi 17 . . . 4  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  E. c
( c  Fn  om  /\ 
A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) ) )
94 simp2 989 . . . . . . . . . 10  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  c  Fn  om )
95 nfra1 2806 . . . . . . . . . . . . 13  |-  F/ n A. n  e.  om  ( c `  n
)  e.  ( C `
 n )
9651, 95nfan 1863 . . . . . . . . . . . 12  |-  F/ n
( A. n  e. 
om  ( b `  n )  e.  B  /\  A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) )
97 rsp 2887 . . . . . . . . . . . . . . . 16  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( n  e.  om  ->  ( c `  n )  e.  ( C `  n ) ) )
9897com12 31 . . . . . . . . . . . . . . 15  |-  ( n  e.  om  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
( c `  n
)  e.  ( C `
 n ) ) )
99 rsp 2887 . . . . . . . . . . . . . . . . . 18  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( n  e.  om  ->  (
b `  n )  e.  B ) )
10099com12 31 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  om  ->  ( A. n  e.  om  ( b `  n
)  e.  B  -> 
( b `  n
)  e.  B ) )
10180eleq2d 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  om  ->  (
( c `  n
)  e.  ( C `
 n )  <->  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) ) )
102 eldifi 3579 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c `  n )  e.  ( ( b `
 n )  \  U_ k  e.  n  ( b `  k
) )  ->  (
c `  n )  e.  ( b `  n
) )
103101, 102syl6bi 228 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  om  ->  (
( c `  n
)  e.  ( C `
 n )  -> 
( c `  n
)  e.  ( b `
 n ) ) )
10458simplbi 460 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b `  n )  e.  B  ->  (
b `  n )  C_  A )
105104sseld 3456 . . . . . . . . . . . . . . . . . 18  |-  ( ( b `  n )  e.  B  ->  (
( c `  n
)  e.  ( b `
 n )  -> 
( c `  n
)  e.  A ) )
106103, 105syl9 71 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  om  ->  (
( b `  n
)  e.  B  -> 
( ( c `  n )  e.  ( C `  n )  ->  ( c `  n )  e.  A
) ) )
107100, 106syld 44 . . . . . . . . . . . . . . . 16  |-  ( n  e.  om  ->  ( A. n  e.  om  ( b `  n
)  e.  B  -> 
( ( c `  n )  e.  ( C `  n )  ->  ( c `  n )  e.  A
) ) )
108107com23 78 . . . . . . . . . . . . . . 15  |-  ( n  e.  om  ->  (
( c `  n
)  e.  ( C `
 n )  -> 
( A. n  e. 
om  ( b `  n )  e.  B  ->  ( c `  n
)  e.  A ) ) )
10998, 108syld 44 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
( A. n  e. 
om  ( b `  n )  e.  B  ->  ( c `  n
)  e.  A ) ) )
110109com13 80 . . . . . . . . . . . . 13  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( n  e.  om  ->  ( c `  n )  e.  A
) ) )
111110imp 429 . . . . . . . . . . . 12  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  (
n  e.  om  ->  ( c `  n )  e.  A ) )
11296, 111ralrimi 2818 . . . . . . . . . . 11  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  A. n  e.  om  ( c `  n )  e.  A
)
1131123adant2 1007 . . . . . . . . . 10  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  A. n  e.  om  ( c `  n )  e.  A
)
114 ffnfv 5971 . . . . . . . . . 10  |-  ( c : om --> A  <->  ( c  Fn  om  /\  A. n  e.  om  ( c `  n )  e.  A
) )
11594, 113, 114sylanbrc 664 . . . . . . . . 9  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  c : om --> A )
116 nfv 1674 . . . . . . . . . . . 12  |-  F/ n  k  e.  om
117 nnord 6587 . . . . . . . . . . . . . . . 16  |-  ( k  e.  om  ->  Ord  k )
118 nnord 6587 . . . . . . . . . . . . . . . 16  |-  ( n  e.  om  ->  Ord  n )
119 ordtri3or 4852 . . . . . . . . . . . . . . . 16  |-  ( ( Ord  k  /\  Ord  n )  ->  (
k  e.  n  \/  k  =  n  \/  n  e.  k ) )
120117, 118, 119syl2an 477 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  om  /\  n  e.  om )  ->  ( k  e.  n  \/  k  =  n  \/  n  e.  k
) )
12197, 101mpbidi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( n  e.  om  ->  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) ) )
12295, 121ralrimi 2818 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  A. n  e.  om  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) )
123 fveq2 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  (
c `  n )  =  ( c `  k ) )
124 fveq2 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  j  ->  (
b `  k )  =  ( b `  j ) )
125124cbviunv 4310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  U_ k  e.  n  ( b `  k )  =  U_ j  e.  n  (
b `  j )
126 iuneq1 4285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  U_ j  e.  n  ( b `  j )  =  U_ j  e.  k  (
b `  j )
)
127125, 126syl5eq 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  U_ k  e.  n  ( b `  k )  =  U_ j  e.  k  (
b `  j )
)
12861, 127difeq12d 3576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  (
( b `  n
)  \  U_ k  e.  n  ( b `  k ) )  =  ( ( b `  k )  \  U_ j  e.  k  (
b `  j )
) )
129123, 128eleq12d 2533 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( n  =  k  ->  (
( c `  n
)  e.  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) )  <->  ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) ) ) )
130129rspccv 3169 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A. n  e.  om  (
c `  n )  e.  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
)  ->  ( k  e.  om  ->  ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) ) ) )
131122, 130syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( k  e.  om  ->  ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) ) ) )
132131com12 31 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  om  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
( c `  k
)  e.  ( ( b `  k ) 
\  U_ j  e.  k  ( b `  j
) ) ) )
1331323ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( A. n  e. 
om  ( c `  n )  e.  ( C `  n )  ->  ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) ) ) )
134 eldifi 3579 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c `  k )  e.  ( ( b `
 k )  \  U_ j  e.  k 
( b `  j
) )  ->  (
c `  k )  e.  ( b `  k
) )
135 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( b `
 k )  <->  ( c `  n )  e.  ( b `  k ) ) )
136134, 135syl5ib 219 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( ( b `  k ) 
\  U_ j  e.  k  ( b `  j
) )  ->  (
c `  n )  e.  ( b `  k
) ) )
1371363ad2ant3 1011 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) )  -> 
( c `  n
)  e.  ( b `
 k ) ) )
138133, 137syld 44 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( A. n  e. 
om  ( c `  n )  e.  ( C `  n )  ->  ( c `  n )  e.  ( b `  k ) ) )
139138imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  ( b `  k ) )
140 ssiun2 4314 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  n  ->  (
b `  k )  C_ 
U_ k  e.  n  ( b `  k
) )
141140sseld 3456 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  n  ->  (
( c `  n
)  e.  ( b `
 k )  -> 
( c `  n
)  e.  U_ k  e.  n  ( b `  k ) ) )
142139, 141syl5 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  n  ->  (
( ( k  e. 
om  /\  n  e.  om 
/\  ( c `  k )  =  ( c `  n ) )  /\  A. n  e.  om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  U_ k  e.  n  (
b `  k )
) )
1431423impib 1186 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  n  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  U_ k  e.  n  (
b `  k )
)
144121com12 31 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
( c `  n
)  e.  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) ) ) )
1451443ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( A. n  e. 
om  ( c `  n )  e.  ( C `  n )  ->  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) ) )
146145imp 429 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) )
147146eldifbd 3442 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  -.  (
c `  n )  e.  U_ k  e.  n  ( b `  k
) )
1481473adant1 1006 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  n  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  -.  (
c `  n )  e.  U_ k  e.  n  ( b `  k
) )
149143, 148pm2.21dd 174 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  n  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  k  =  n )
1501493exp 1187 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  n  ->  (
( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
151 ax-1 6 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  n  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
k  =  n ) )
152151a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  (
( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
153 fveq2 5792 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  n  ->  (
b `  j )  =  ( b `  n ) )
154153ssiun2s 4315 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  k  ->  (
b `  n )  C_ 
U_ j  e.  k  ( b `  j
) )
155154sseld 3456 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  k  ->  (
( c `  n
)  e.  ( b `
 n )  -> 
( c `  n
)  e.  U_ j  e.  k  ( b `  j ) ) )
156102, 155syl5 32 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  k  ->  (
( c `  n
)  e.  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) )  ->  (
c `  n )  e.  U_ j  e.  k  ( b `  j
) ) )
157146, 156syl5 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  k  ->  (
( ( k  e. 
om  /\  n  e.  om 
/\  ( c `  k )  =  ( c `  n ) )  /\  A. n  e.  om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  U_ j  e.  k  (
b `  j )
) )
1581573impib 1186 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  k  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  ( c `  n )  e.  U_ j  e.  k  (
b `  j )
)
159 eleq1 2523 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( ( b `  k ) 
\  U_ j  e.  k  ( b `  j
) )  <->  ( c `  n )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) ) ) )
160 eldifn 3580 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  n )  e.  ( ( b `
 k )  \  U_ j  e.  k 
( b `  j
) )  ->  -.  ( c `  n
)  e.  U_ j  e.  k  ( b `  j ) )
161159, 160syl6bi 228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( ( b `  k ) 
\  U_ j  e.  k  ( b `  j
) )  ->  -.  ( c `  n
)  e.  U_ j  e.  k  ( b `  j ) ) )
1621613ad2ant3 1011 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( ( c `  k )  e.  ( ( b `  k
)  \  U_ j  e.  k  ( b `  j ) )  ->  -.  ( c `  n
)  e.  U_ j  e.  k  ( b `  j ) ) )
163133, 162syld 44 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( A. n  e. 
om  ( c `  n )  e.  ( C `  n )  ->  -.  ( c `  n )  e.  U_ j  e.  k  (
b `  j )
) )
164163a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  k  ->  (
( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  -.  ( c `  n )  e.  U_ j  e.  k  (
b `  j )
) ) )
1651643imp 1182 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  k  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  -.  (
c `  n )  e.  U_ j  e.  k  ( b `  j
) )
166158, 165pm2.21dd 174 . . . . . . . . . . . . . . . . . . 19  |-  ( ( n  e.  k  /\  ( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  /\  A. n  e. 
om  ( c `  n )  e.  ( C `  n ) )  ->  k  =  n )
1671663exp 1187 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  k  ->  (
( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
168150, 152, 1673jaoi 1282 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  n  \/  k  =  n  \/  n  e.  k )  ->  ( ( k  e.  om  /\  n  e.  om  /\  ( c `
 k )  =  ( c `  n
) )  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
k  =  n ) ) )
169168com12 31 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  om  /\  n  e.  om  /\  (
c `  k )  =  ( c `  n ) )  -> 
( ( k  e.  n  \/  k  =  n  \/  n  e.  k )  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
k  =  n ) ) )
1701693expia 1190 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  om  /\  n  e.  om )  ->  ( ( c `  k )  =  ( c `  n )  ->  ( ( k  e.  n  \/  k  =  n  \/  n  e.  k )  ->  ( A. n  e.  om  ( c `  n
)  e.  ( C `
 n )  -> 
k  =  n ) ) ) )
171120, 170mpid 41 . . . . . . . . . . . . . 14  |-  ( ( k  e.  om  /\  n  e.  om )  ->  ( ( c `  k )  =  ( c `  n )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
172171com3r 79 . . . . . . . . . . . . 13  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( (
k  e.  om  /\  n  e.  om )  ->  ( ( c `  k )  =  ( c `  n )  ->  k  =  n ) ) )
173172expd 436 . . . . . . . . . . . 12  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( k  e.  om  ->  ( n  e.  om  ->  ( (
c `  k )  =  ( c `  n )  ->  k  =  n ) ) ) )
17495, 116, 173ralrimd 2903 . . . . . . . . . . 11  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( k  e.  om  ->  A. n  e.  om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) ) )
175174ralrimiv 2823 . . . . . . . . . 10  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  A. k  e.  om  A. n  e. 
om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) )
1761753ad2ant3 1011 . . . . . . . . 9  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  A. k  e.  om  A. n  e. 
om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) )
177 dff13 6073 . . . . . . . . 9  |-  ( c : om -1-1-> A  <->  ( c : om --> A  /\  A. k  e.  om  A. n  e.  om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) ) )
178115, 176, 177sylanbrc 664 . . . . . . . 8  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  c : om -1-1-> A )
179 19.8a 1795 . . . . . . . 8  |-  ( c : om -1-1-> A  ->  E. c  c : om
-1-1-> A )
180178, 179syl 16 . . . . . . 7  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  E. c 
c : om -1-1-> A
)
1812brdom 7425 . . . . . . 7  |-  ( om  ~<_  A  <->  E. c  c : om -1-1-> A )
182180, 181sylibr 212 . . . . . 6  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  om  ~<_  A )
1831823expib 1191 . . . . 5  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( ( c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  om  ~<_  A ) )
184183exlimdv 1691 . . . 4  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( E. c ( c  Fn 
om  /\  A. n  e.  om  ( c `  n )  e.  ( C `  n ) )  ->  om  ~<_  A ) )
18593, 184mpd 15 . . 3  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  om  ~<_  A )
186185exlimiv 1689 . 2  |-  ( E. b A. n  e. 
om  ( b `  n )  e.  B  ->  om  ~<_  A )
18748, 186syl 16 1  |-  ( -.  A  e.  Fin  ->  om  ~<_  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    \/ w3o 964    /\ w3a 965    = wceq 1370   E.wex 1587    e. wcel 1758   {cab 2436    =/= wne 2644   A.wral 2795   _Vcvv 3071    \ cdif 3426    C_ wss 3429   (/)c0 3738   ~Pcpw 3961   U_ciun 4272   class class class wbr 4393    |-> cmpt 4451   Ord word 4819   suc csuc 4822   dom cdm 4941    Fn wfn 5514   -->wf 5515   -1-1->wf1 5516   ` cfv 5519   omcom 6579    ~~ cen 7410    ~<_ cdom 7411    ~< csdm 7412   Fincfn 7413   cardccrd 8209
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4504  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-un 6475  ax-inf2 7951  ax-cc 8708
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3073  df-sbc 3288  df-csb 3390  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-pss 3445  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-tp 3983  df-op 3985  df-uni 4193  df-int 4230  df-iun 4274  df-br 4394  df-opab 4452  df-mpt 4453  df-tr 4487  df-eprel 4733  df-id 4737  df-po 4742  df-so 4743  df-fr 4780  df-we 4782  df-ord 4823  df-on 4824  df-lim 4825  df-suc 4826  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-f1 5524  df-fo 5525  df-f1o 5526  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-om 6580  df-1st 6680  df-2nd 6681  df-recs 6935  df-rdg 6969  df-1o 7023  df-2o 7024  df-oadd 7027  df-er 7204  df-map 7319  df-en 7414  df-dom 7415  df-sdom 7416  df-fin 7417  df-card 8213  df-cda 8441
This theorem is referenced by:  domtriom  8716
  Copyright terms: Public domain W3C validator