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

Theorem domtriomlem 8890
Description: Lemma for domtriom 8891. (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 4584 . . . . . 6  |-  ~P A  e.  _V
4 simpl 464 . . . . . . . 8  |-  ( ( y  C_  A  /\  y  ~~  ~P n )  ->  y  C_  A
)
54ss2abi 3487 . . . . . . 7  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  C_  { y  |  y  C_  A }
6 df-pw 3944 . . . . . . 7  |-  ~P A  =  { y  |  y 
C_  A }
75, 6sseqtr4i 3451 . . . . . 6  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  C_  ~P A
83, 7ssexi 4541 . . . . 5  |-  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  e.  _V
91, 8eqeltri 2545 . . . 4  |-  B  e. 
_V
10 omex 8166 . . . . 5  |-  om  e.  _V
1110enref 7620 . . . 4  |-  om  ~~  om
129, 11axcc3 8886 . . 3  |-  E. b
( b  Fn  om  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )
13 nfv 1769 . . . . . . . 8  |-  F/ n  -.  A  e.  Fin
14 nfra1 2785 . . . . . . . 8  |-  F/ n A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B )
1513, 14nfan 2031 . . . . . . 7  |-  F/ n
( -.  A  e. 
Fin  /\  A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) )
16 nnfi 7783 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  n  e.  Fin )
17 pwfi 7887 . . . . . . . . . . . . . 14  |-  ( n  e.  Fin  <->  ~P n  e.  Fin )
1816, 17sylib 201 . . . . . . . . . . . . 13  |-  ( n  e.  om  ->  ~P n  e.  Fin )
19 ficardom 8413 . . . . . . . . . . . . 13  |-  ( ~P n  e.  Fin  ->  (
card `  ~P n
)  e.  om )
20 isinf 7803 . . . . . . . . . . . . . 14  |-  ( -.  A  e.  Fin  ->  A. m  e.  om  E. y ( y  C_  A  /\  y  ~~  m
) )
21 breq2 4399 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( card `  ~P n )  ->  (
y  ~~  m  <->  y  ~~  ( card `  ~P n
) ) )
2221anbi2d 718 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( card `  ~P n )  ->  (
( y  C_  A  /\  y  ~~  m )  <-> 
( y  C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2322exbidv 1776 . . . . . . . . . . . . . . 15  |-  ( m  =  ( card `  ~P n )  ->  ( E. y ( y  C_  A  /\  y  ~~  m
)  <->  E. y ( y 
C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
2423rspcv 3132 . . . . . . . . . . . . . 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 18 . . . . . . . . . . . 12  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  E. y ( y 
C_  A  /\  y  ~~  ( card `  ~P n ) ) ) )
27 finnum 8400 . . . . . . . . . . . . . . 15  |-  ( ~P n  e.  Fin  ->  ~P n  e.  dom  card )
28 cardid2 8405 . . . . . . . . . . . . . . 15  |-  ( ~P n  e.  dom  card  -> 
( card `  ~P n
)  ~~  ~P n
)
29 entr 7639 . . . . . . . . . . . . . . . 16  |-  ( ( y  ~~  ( card `  ~P n )  /\  ( card `  ~P n
)  ~~  ~P n
)  ->  y  ~~  ~P n )
3029expcom 442 . . . . . . . . . . . . . . 15  |-  ( (
card `  ~P n
)  ~~  ~P n  ->  ( y  ~~  ( card `  ~P n )  ->  y  ~~  ~P n ) )
3118, 27, 28, 304syl 19 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  (
y  ~~  ( card `  ~P n )  -> 
y  ~~  ~P n
) )
3231anim2d 575 . . . . . . . . . . . . 13  |-  ( n  e.  om  ->  (
( y  C_  A  /\  y  ~~  ( card `  ~P n ) )  ->  ( y  C_  A  /\  y  ~~  ~P n ) ) )
3332eximdv 1772 . . . . . . . . . . . 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 2707 . . . . . . . . . . . 12  |-  ( B  =/=  (/)  <->  { y  |  ( y  C_  A  /\  y  ~~  ~P n ) }  =/=  (/) )
36 abn0 3754 . . . . . . . . . . . 12  |-  ( { y  |  ( y 
C_  A  /\  y  ~~  ~P n ) }  =/=  (/)  <->  E. y ( y 
C_  A  /\  y  ~~  ~P n ) )
3735, 36bitri 257 . . . . . . . . . . 11  |-  ( B  =/=  (/)  <->  E. y ( y 
C_  A  /\  y  ~~  ~P n ) )
3834, 37syl6ibr 235 . . . . . . . . . 10  |-  ( n  e.  om  ->  ( -.  A  e.  Fin  ->  B  =/=  (/) ) )
3938com12 31 . . . . . . . . 9  |-  ( -.  A  e.  Fin  ->  ( n  e.  om  ->  B  =/=  (/) ) )
4039adantr 472 . . . . . . . 8  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  -> 
( n  e.  om  ->  B  =/=  (/) ) )
41 rsp 2773 . . . . . . . . 9  |-  ( A. n  e.  om  ( B  =/=  (/)  ->  ( b `  n )  e.  B
)  ->  ( n  e.  om  ->  ( B  =/=  (/)  ->  ( b `  n )  e.  B
) ) )
4241adantl 473 . . . . . . . 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 2800 . . . . . 6  |-  ( ( -.  A  e.  Fin  /\ 
A. n  e.  om  ( B  =/=  (/)  ->  (
b `  n )  e.  B ) )  ->  A. n  e.  om  ( b `  n
)  e.  B )
45443adant2 1049 . . . . 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 1234 . . . 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 1772 . . 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 20 . 2  |-  ( -.  A  e.  Fin  ->  E. b A. n  e. 
om  ( b `  n )  e.  B
)
49 axcc2 8885 . . . . 5  |-  E. c
( c  Fn  om  /\ 
A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )
50 simp2 1031 . . . . . . . 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 2785 . . . . . . . . . . 11  |-  F/ n A. n  e.  om  ( b `  n
)  e.  B
52 nfra1 2785 . . . . . . . . . . 11  |-  F/ n A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) )
5351, 52nfan 2031 . . . . . . . . . 10  |-  F/ n
( A. n  e. 
om  ( b `  n )  e.  B  /\  A. n  e.  om  ( ( C `  n )  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) )
54 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( b `
 n )  e. 
_V
55 sseq1 3439 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( b `  n )  ->  (
y  C_  A  <->  ( b `  n )  C_  A
) )
56 breq1 4398 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( b `  n )  ->  (
y  ~~  ~P n  <->  ( b `  n ) 
~~  ~P n ) )
5755, 56anbi12d 725 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( b `  n )  ->  (
( y  C_  A  /\  y  ~~  ~P n
)  <->  ( ( b `
 n )  C_  A  /\  ( b `  n )  ~~  ~P n ) ) )
5854, 57, 1elab2 3176 . . . . . . . . . . . . . . 15  |-  ( ( b `  n )  e.  B  <->  ( (
b `  n )  C_  A  /\  ( b `
 n )  ~~  ~P n ) )
5958simprbi 471 . . . . . . . . . . . . . 14  |-  ( ( b `  n )  e.  B  ->  (
b `  n )  ~~  ~P n )
6059ralimi 2796 . . . . . . . . . . . . 13  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  A. n  e.  om  ( b `  n )  ~~  ~P n )
61 fveq2 5879 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  (
b `  n )  =  ( b `  k ) )
62 pweq 3945 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  ~P n  =  ~P k
)
6361, 62breq12d 4408 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  (
( b `  n
)  ~~  ~P n  <->  ( b `  k ) 
~~  ~P k ) )
6463cbvralv 3005 . . . . . . . . . . . . . . 15  |-  ( A. n  e.  om  (
b `  n )  ~~  ~P n  <->  A. k  e.  om  ( b `  k )  ~~  ~P k )
65 peano2 6732 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  om  ->  suc  n  e.  om )
66 omelon 8169 . . . . . . . . . . . . . . . . . . 19  |-  om  e.  On
6766onelssi 5538 . . . . . . . . . . . . . . . . . 18  |-  ( suc  n  e.  om  ->  suc  n  C_  om )
68 ssralv 3479 . . . . . . . . . . . . . . . . . 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 18 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  om  ->  ( A. k  e.  om  ( b `  k
)  ~~  ~P k  ->  A. k  e.  suc  n ( b `  k )  ~~  ~P k ) )
70 pwsdompw 8652 . . . . . . . . . . . . . . . . . 18  |-  ( ( n  e.  om  /\  A. k  e.  suc  n
( b `  k
)  ~~  ~P k
)  ->  U_ k  e.  n  ( b `  k )  ~<  (
b `  n )
)
7170ex 441 . . . . . . . . . . . . . . . . 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 7738 . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  ( A. n  e.  om  ( b `  n
)  ~~  ~P n  ->  ( ( b `  n )  \  U_ k  e.  n  (
b `  k )
)  =/=  (/) ) )
76 difss 3549 . . . . . . . . . . . . . . . . 17  |-  ( ( b `  n ) 
\  U_ k  e.  n  ( b `  k
) )  C_  (
b `  n )
7754, 76ssexi 4541 . . . . . . . . . . . . . . . 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 5972 . . . . . . . . . . . . . . . 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 685 . . . . . . . . . . . . . . 15  |-  ( n  e.  om  ->  ( C `  n )  =  ( ( b `
 n )  \  U_ k  e.  n  ( b `  k
) ) )
8180neeq1d 2702 . . . . . . . . . . . . . 14  |-  ( n  e.  om  ->  (
( C `  n
)  =/=  (/)  <->  ( (
b `  n )  \  U_ k  e.  n  ( b `  k
) )  =/=  (/) ) )
8275, 81sylibrd 242 . . . . . . . . . . . . 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 472 . . . . . . . . . . 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 2773 . . . . . . . . . . . 12  |-  ( A. n  e.  om  (
( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) )  ->  (
n  e.  om  ->  ( ( C `  n
)  =/=  (/)  ->  (
c `  n )  e.  ( C `  n
) ) ) )
8685adantl 473 . . . . . . . . . . 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 2800 . . . . . . . . 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 1049 . . . . . . . 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 541 . . . . . . 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 1234 . . . . . 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 1772 . . . . 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 20 . . . 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 1031 . . . . . . . . . 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 2785 . . . . . . . . . . . . 13  |-  F/ n A. n  e.  om  ( c `  n
)  e.  ( C `
 n )
9651, 95nfan 2031 . . . . . . . . . . . 12  |-  F/ n
( A. n  e. 
om  ( b `  n )  e.  B  /\  A. n  e.  om  ( c `  n
)  e.  ( C `
 n ) )
97 rsp 2773 . . . . . . . . . . . . . . . 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 2773 . . . . . . . . . . . . . . . . . 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 2534 . . . . . . . . . . . . . . . . . . 19  |-  ( n  e.  om  ->  (
( c `  n
)  e.  ( C `
 n )  <->  ( c `  n )  e.  ( ( b `  n
)  \  U_ k  e.  n  ( b `  k ) ) ) )
102 eldifi 3544 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c `  n )  e.  ( ( b `
 n )  \  U_ k  e.  n  ( b `  k
) )  ->  (
c `  n )  e.  ( b `  n
) )
103101, 102syl6bi 236 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  om  ->  (
( c `  n
)  e.  ( C `
 n )  -> 
( c `  n
)  e.  ( b `
 n ) ) )
10458simplbi 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( b `  n )  e.  B  ->  (
b `  n )  C_  A )
105104sseld 3417 . . . . . . . . . . . . . . . . . 18  |-  ( ( b `  n )  e.  B  ->  (
( c `  n
)  e.  ( b `
 n )  -> 
( c `  n
)  e.  A ) )
106103, 105syl9 72 . . . . . . . . . . . . . . . . 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 80 . . . . . . . . . . . . . . 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 82 . . . . . . . . . . . . 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 436 . . . . . . . . . . . 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 2800 . . . . . . . . . . 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 1049 . . . . . . . . . 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 6064 . . . . . . . . . 10  |-  ( c : om --> A  <->  ( c  Fn  om  /\  A. n  e.  om  ( c `  n )  e.  A
) )
11594, 113, 114sylanbrc 677 . . . . . . . . 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 1769 . . . . . . . . . . . 12  |-  F/ n  k  e.  om
117 nnord 6719 . . . . . . . . . . . . . . . 16  |-  ( k  e.  om  ->  Ord  k )
118 nnord 6719 . . . . . . . . . . . . . . . 16  |-  ( n  e.  om  ->  Ord  n )
119 ordtri3or 5462 . . . . . . . . . . . . . . . 16  |-  ( ( Ord  k  /\  Ord  n )  ->  (
k  e.  n  \/  k  =  n  \/  n  e.  k ) )
120117, 118, 119syl2an 485 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  om  /\  n  e.  om )  ->  ( k  e.  n  \/  k  =  n  \/  n  e.  k
) )
12197, 101mpbidi 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  (
c `  n )  =  ( c `  k ) )
124 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( k  =  j  ->  (
b `  k )  =  ( b `  j ) )
125124cbviunv 4308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  U_ k  e.  n  ( b `  k )  =  U_ j  e.  n  (
b `  j )
126 iuneq1 4283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( n  =  k  ->  U_ j  e.  n  ( b `  j )  =  U_ j  e.  k  (
b `  j )
)
127125, 126syl5eq 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( n  =  k  ->  U_ k  e.  n  ( b `  k )  =  U_ j  e.  k  (
b `  j )
)
12861, 127difeq12d 3541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  =  k  ->  (
( b `  n
)  \  U_ k  e.  n  ( b `  k ) )  =  ( ( b `  k )  \  U_ j  e.  k  (
b `  j )
) )
129123, 128eleq12d 2543 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3133 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1051 . . . . . . . . . . . . . . . . . . . . . . . 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 3544 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c `  k )  e.  ( ( b `
 k )  \  U_ j  e.  k 
( b `  j
) )  ->  (
c `  k )  e.  ( b `  k
) )
135 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( b `
 k )  <->  ( c `  n )  e.  ( b `  k ) ) )
136134, 135syl5ib 227 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  k )  =  ( c `  n )  ->  (
( c `  k
)  e.  ( ( b `  k ) 
\  U_ j  e.  k  ( b `  j
) )  ->  (
c `  n )  e.  ( b `  k
) ) )
1371363ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . 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 4312 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  n  ->  (
b `  k )  C_ 
U_ k  e.  n  ( b `  k
) )
141140sseld 3417 . . . . . . . . . . . . . . . . . . . . . 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 1229 . . . . . . . . . . . . . . . . . . . 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 1052 . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . 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 3403 . . . . . . . . . . . . . . . . . . . . 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 1048 . . . . . . . . . . . . . . . . . . . 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 179 . . . . . . . . . . . . . . . . . . 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 1230 . . . . . . . . . . . . . . . . . 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 2a1 27 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  n  ->  (
( k  e.  om  /\  n  e.  om  /\  ( c `  k
)  =  ( c `
 n ) )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
152 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  n  ->  (
b `  j )  =  ( b `  n ) )
153152ssiun2s 4313 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  k  ->  (
b `  n )  C_ 
U_ j  e.  k  ( b `  j
) )
154153sseld 3417 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  k  ->  (
( c `  n
)  e.  ( b `
 n )  -> 
( c `  n
)  e.  U_ j  e.  k  ( b `  j ) ) )
155102, 154syl5 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
) ) )
156146, 155syl5 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 )
) )
1571563impib 1229 . . . . . . . . . . . . . . . . . . . 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 )
)
158 eleq1 2537 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
159 eldifn 3545 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( c `  n )  e.  ( ( b `
 k )  \  U_ j  e.  k 
( b `  j
) )  ->  -.  ( c `  n
)  e.  U_ j  e.  k  ( b `  j ) )
160158, 159syl6bi 236 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
1611603ad2ant3 1053 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
162133, 161syld 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 )
) )
163162a1i 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 )
) ) )
1641633imp 1224 . . . . . . . . . . . . . . . . . . . 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
) )
165157, 164pm2.21dd 179 . . . . . . . . . . . . . . . . . . 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 )
1661653exp 1230 . . . . . . . . . . . . . . . . . 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 ) ) )
167150, 151, 1663jaoi 1357 . . . . . . . . . . . . . . . . 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 ) ) )
168167com12 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 ) ) )
1691683expia 1233 . . . . . . . . . . . . . . 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 ) ) ) )
170120, 169mpid 41 . . . . . . . . . . . . . 14  |-  ( ( k  e.  om  /\  n  e.  om )  ->  ( ( c `  k )  =  ( c `  n )  ->  ( A. n  e.  om  ( c `  n )  e.  ( C `  n )  ->  k  =  n ) ) )
171170com3r 81 . . . . . . . . . . . . 13  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( (
k  e.  om  /\  n  e.  om )  ->  ( ( c `  k )  =  ( c `  n )  ->  k  =  n ) ) )
172171expd 443 . . . . . . . . . . . 12  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( k  e.  om  ->  ( n  e.  om  ->  ( (
c `  k )  =  ( c `  n )  ->  k  =  n ) ) ) )
17395, 116, 172ralrimd 2802 . . . . . . . . . . 11  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  ( k  e.  om  ->  A. n  e.  om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) ) )
174173ralrimiv 2808 . . . . . . . . . 10  |-  ( A. n  e.  om  (
c `  n )  e.  ( C `  n
)  ->  A. k  e.  om  A. n  e. 
om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) )
1751743ad2ant3 1053 . . . . . . . . 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 ) )
176 dff13 6177 . . . . . . . . 9  |-  ( c : om -1-1-> A  <->  ( c : om --> A  /\  A. k  e.  om  A. n  e.  om  ( ( c `
 k )  =  ( c `  n
)  ->  k  =  n ) ) )
177115, 175, 176sylanbrc 677 . . . . . . . 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 )
178 19.8a 1955 . . . . . . . 8  |-  ( c : om -1-1-> A  ->  E. c  c : om
-1-1-> A )
179177, 178syl 17 . . . . . . 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
)
1802brdom 7599 . . . . . . 7  |-  ( om  ~<_  A  <->  E. c  c : om -1-1-> A )
181179, 180sylibr 217 . . . . . 6  |-  ( ( A. n  e.  om  ( b `  n
)  e.  B  /\  c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  om  ~<_  A )
1821813expib 1234 . . . . 5  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  ( ( c  Fn  om  /\  A. n  e.  om  (
c `  n )  e.  ( C `  n
) )  ->  om  ~<_  A ) )
183182exlimdv 1787 . . . 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 ) )
18493, 183mpd 15 . . 3  |-  ( A. n  e.  om  (
b `  n )  e.  B  ->  om  ~<_  A )
185184exlimiv 1784 . 2  |-  ( E. b A. n  e. 
om  ( b `  n )  e.  B  ->  om  ~<_  A )
18648, 185syl 17 1  |-  ( -.  A  e.  Fin  ->  om  ~<_  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 376    \/ w3o 1006    /\ w3a 1007    = wceq 1452   E.wex 1671    e. wcel 1904   {cab 2457    =/= wne 2641   A.wral 2756   _Vcvv 3031    \ cdif 3387    C_ wss 3390   (/)c0 3722   ~Pcpw 3942   U_ciun 4269   class class class wbr 4395    |-> cmpt 4454   dom cdm 4839   Ord word 5429   suc csuc 5432    Fn wfn 5584   -->wf 5585   -1-1->wf1 5586   ` cfv 5589   omcom 6711    ~~ cen 7584    ~<_ cdom 7585    ~< csdm 7586   Fincfn 7587   cardccrd 8387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cc 8883
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-card 8391  df-cda 8616
This theorem is referenced by:  domtriom  8891
  Copyright terms: Public domain W3C validator