Metamath Proof Explorer

Theorem constrfiss

Description: For any finite set A of constructible numbers, there is a n -th step ( Cn ) containing all numbers in A . (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Hypotheses constr0.1 
|- C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
constrfiss.1 
|- ( ph -> A C_ Constr )
constrfiss.2 
|- ( ph -> A e. Fin )
Assertion constrfiss 
|- ( ph -> E. n e. _om A C_ ( C ` n ) )

Proof

Step Hyp Ref Expression
1 constr0.1 
 |-  C = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )
2 constrfiss.1 
 |-  ( ph -> A C_ Constr )
3 constrfiss.2 
 |-  ( ph -> A e. Fin )
4 sseq1 
 |-  ( b = (/) -> ( b C_ ( C ` n ) <-> (/) C_ ( C ` n ) ) )
5 4 rexbidv 
 |-  ( b = (/) -> ( E. n e. _om b C_ ( C ` n ) <-> E. n e. _om (/) C_ ( C ` n ) ) )
6 sseq1 
 |-  ( b = i -> ( b C_ ( C ` n ) <-> i C_ ( C ` n ) ) )
7 6 rexbidv 
 |-  ( b = i -> ( E. n e. _om b C_ ( C ` n ) <-> E. n e. _om i C_ ( C ` n ) ) )
8 sseq1 
 |-  ( b = ( i u. { x } ) -> ( b C_ ( C ` n ) <-> ( i u. { x } ) C_ ( C ` n ) ) )
9 8 rexbidv 
 |-  ( b = ( i u. { x } ) -> ( E. n e. _om b C_ ( C ` n ) <-> E. n e. _om ( i u. { x } ) C_ ( C ` n ) ) )
10 fveq2 
 |-  ( n = m -> ( C ` n ) = ( C ` m ) )
11 10 sseq2d 
 |-  ( n = m -> ( ( i u. { x } ) C_ ( C ` n ) <-> ( i u. { x } ) C_ ( C ` m ) ) )
12 11 cbvrexvw 
 |-  ( E. n e. _om ( i u. { x } ) C_ ( C ` n ) <-> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
13 9 12 bitrdi 
 |-  ( b = ( i u. { x } ) -> ( E. n e. _om b C_ ( C ` n ) <-> E. m e. _om ( i u. { x } ) C_ ( C ` m ) ) )
14 sseq1 
 |-  ( b = A -> ( b C_ ( C ` n ) <-> A C_ ( C ` n ) ) )
15 14 rexbidv 
 |-  ( b = A -> ( E. n e. _om b C_ ( C ` n ) <-> E. n e. _om A C_ ( C ` n ) ) )
16 peano1 
 |-  (/) e. _om
17 16 ne0ii 
 |-  _om =/= (/)
18 0ss 
 |-  (/) C_ ( C ` n )
19 18 a1i 
 |-  ( ( ph /\ n e. _om ) -> (/) C_ ( C ` n ) )
20 19 reximdva0 
 |-  ( ( ph /\ _om =/= (/) ) -> E. n e. _om (/) C_ ( C ` n ) )
21 17 20 mpan2 
 |-  ( ph -> E. n e. _om (/) C_ ( C ` n ) )
22 simpllr 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> l e. _om )
23 fveq2 
 |-  ( m = l -> ( C ` m ) = ( C ` l ) )
24 23 sseq2d 
 |-  ( m = l -> ( ( i u. { x } ) C_ ( C ` m ) <-> ( i u. { x } ) C_ ( C ` l ) ) )
25 24 adantl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) /\ m = l ) -> ( ( i u. { x } ) C_ ( C ` m ) <-> ( i u. { x } ) C_ ( C ` l ) ) )
26 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> i C_ ( C ` n ) )
27 nnon 
 |-  ( l e. _om -> l e. On )
28 27 adantr 
 |-  ( ( l e. _om /\ n e. l ) -> l e. On )
29 simpr 
 |-  ( ( l e. _om /\ n e. l ) -> n e. l )
30 1 28 29 constrmon 
 |-  ( ( l e. _om /\ n e. l ) -> ( C ` n ) C_ ( C ` l ) )
31 22 30 sylancom 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> ( C ` n ) C_ ( C ` l ) )
32 26 31 sstrd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> i C_ ( C ` l ) )
33 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> x e. ( C ` l ) )
34 33 snssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> { x } C_ ( C ` l ) )
35 32 34 unssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> ( i u. { x } ) C_ ( C ` l ) )
36 22 25 35 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n e. l ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
37 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> n e. _om )
38 fveq2 
 |-  ( m = n -> ( C ` m ) = ( C ` n ) )
39 38 sseq2d 
 |-  ( m = n -> ( ( i u. { x } ) C_ ( C ` m ) <-> ( i u. { x } ) C_ ( C ` n ) ) )
40 39 adantl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) /\ m = n ) -> ( ( i u. { x } ) C_ ( C ` m ) <-> ( i u. { x } ) C_ ( C ` n ) ) )
41 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> i C_ ( C ` n ) )
42 nnon 
 |-  ( n e. _om -> n e. On )
43 42 adantr 
 |-  ( ( n e. _om /\ l e. n ) -> n e. On )
44 simpr 
 |-  ( ( n e. _om /\ l e. n ) -> l e. n )
45 1 43 44 constrmon 
 |-  ( ( n e. _om /\ l e. n ) -> ( C ` l ) C_ ( C ` n ) )
46 37 45 sylancom 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> ( C ` l ) C_ ( C ` n ) )
47 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> x e. ( C ` l ) )
48 46 47 sseldd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> x e. ( C ` n ) )
49 48 snssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> { x } C_ ( C ` n ) )
50 41 49 unssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> ( i u. { x } ) C_ ( C ` n ) )
51 37 40 50 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ l e. n ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
52 simp-5r 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> n e. _om )
53 39 adantl 
 |-  ( ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) /\ m = n ) -> ( ( i u. { x } ) C_ ( C ` m ) <-> ( i u. { x } ) C_ ( C ` n ) ) )
54 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> i C_ ( C ` n ) )
55 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> x e. ( C ` l ) )
56 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> n = l )
57 56 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> ( C ` n ) = ( C ` l ) )
58 55 57 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> x e. ( C ` n ) )
59 58 snssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> { x } C_ ( C ` n ) )
60 54 59 unssd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> ( i u. { x } ) C_ ( C ` n ) )
61 52 53 60 rspcedvd 
 |-  ( ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) /\ n = l ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
62 42 ad4antlr 
 |-  ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) -> n e. On )
63 27 ad2antlr 
 |-  ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) -> l e. On )
64 oneltri 
 |-  ( ( n e. On /\ l e. On ) -> ( n e. l \/ l e. n \/ n = l ) )
65 62 63 64 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) -> ( n e. l \/ l e. n \/ n = l ) )
66 36 51 61 65 mpjao3dan 
 |-  ( ( ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) /\ l e. _om ) /\ x e. ( C ` l ) ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
67 2 ad4antr 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> A C_ Constr )
68 simpllr 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> x e. ( A \ i ) )
69 68 eldifad 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> x e. A )
70 67 69 sseldd 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> x e. Constr )
71 1 isconstr 
 |-  ( x e. Constr <-> E. l e. _om x e. ( C ` l ) )
72 70 71 sylib 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> E. l e. _om x e. ( C ` l ) )
73 66 72 r19.29a 
 |-  ( ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ n e. _om ) /\ i C_ ( C ` n ) ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
74 73 r19.29an 
 |-  ( ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) /\ E. n e. _om i C_ ( C ` n ) ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) )
75 74 ex 
 |-  ( ( ( ph /\ i C_ A ) /\ x e. ( A \ i ) ) -> ( E. n e. _om i C_ ( C ` n ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) ) )
76 75 anasss 
 |-  ( ( ph /\ ( i C_ A /\ x e. ( A \ i ) ) ) -> ( E. n e. _om i C_ ( C ` n ) -> E. m e. _om ( i u. { x } ) C_ ( C ` m ) ) )
77 5 7 13 15 21 76 3 findcard2d 
 |-  ( ph -> E. n e. _om A C_ ( C ` n ) )