Metamath Proof Explorer

Theorem onfununi

Description: A property of functions on ordinal numbers. Generalization of Theorem Schema 8E of Enderton p. 218. (Contributed by Eric Schmidt, 26-May-2009)

Ref Expression
Hypotheses onfununi.1 
|- ( Lim y -> ( F ` y ) = U_ x e. y ( F ` x ) )
onfununi.2 
|- ( ( x e. On /\ y e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) )
Assertion onfununi 
|- ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( F ` U. S ) = U_ x e. S ( F ` x ) )

Proof

Step Hyp Ref Expression
1 onfununi.1 
 |-  ( Lim y -> ( F ` y ) = U_ x e. y ( F ` x ) )
2 onfununi.2 
 |-  ( ( x e. On /\ y e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) )
3 ssorduni 
 |-  ( S C_ On -> Ord U. S )
4 3 ad2antrr 
 |-  ( ( ( S C_ On /\ -. U. S e. S ) /\ S =/= (/) ) -> Ord U. S )
5 nelneq 
 |-  ( ( x e. S /\ -. U. S e. S ) -> -. x = U. S )
6 elssuni 
 |-  ( x e. S -> x C_ U. S )
7 6 adantl 
 |-  ( ( S C_ On /\ x e. S ) -> x C_ U. S )
8 ssel 
 |-  ( S C_ On -> ( x e. S -> x e. On ) )
9 eloni 
 |-  ( x e. On -> Ord x )
10 8 9 syl6 
 |-  ( S C_ On -> ( x e. S -> Ord x ) )
11 10 imp 
 |-  ( ( S C_ On /\ x e. S ) -> Ord x )
12 ordsseleq 
 |-  ( ( Ord x /\ Ord U. S ) -> ( x C_ U. S <-> ( x e. U. S \/ x = U. S ) ) )
13 11 3 12 syl2an 
 |-  ( ( ( S C_ On /\ x e. S ) /\ S C_ On ) -> ( x C_ U. S <-> ( x e. U. S \/ x = U. S ) ) )
14 13 anabss1 
 |-  ( ( S C_ On /\ x e. S ) -> ( x C_ U. S <-> ( x e. U. S \/ x = U. S ) ) )
15 7 14 mpbid 
 |-  ( ( S C_ On /\ x e. S ) -> ( x e. U. S \/ x = U. S ) )
16 15 ord 
 |-  ( ( S C_ On /\ x e. S ) -> ( -. x e. U. S -> x = U. S ) )
17 16 con1d 
 |-  ( ( S C_ On /\ x e. S ) -> ( -. x = U. S -> x e. U. S ) )
18 5 17 syl5 
 |-  ( ( S C_ On /\ x e. S ) -> ( ( x e. S /\ -. U. S e. S ) -> x e. U. S ) )
19 18 exp4b 
 |-  ( S C_ On -> ( x e. S -> ( x e. S -> ( -. U. S e. S -> x e. U. S ) ) ) )
20 19 pm2.43d 
 |-  ( S C_ On -> ( x e. S -> ( -. U. S e. S -> x e. U. S ) ) )
21 20 com23 
 |-  ( S C_ On -> ( -. U. S e. S -> ( x e. S -> x e. U. S ) ) )
22 21 imp 
 |-  ( ( S C_ On /\ -. U. S e. S ) -> ( x e. S -> x e. U. S ) )
23 22 ssrdv 
 |-  ( ( S C_ On /\ -. U. S e. S ) -> S C_ U. S )
24 ssn0 
 |-  ( ( S C_ U. S /\ S =/= (/) ) -> U. S =/= (/) )
25 23 24 sylan 
 |-  ( ( ( S C_ On /\ -. U. S e. S ) /\ S =/= (/) ) -> U. S =/= (/) )
26 23 unissd 
 |-  ( ( S C_ On /\ -. U. S e. S ) -> U. S C_ U. U. S )
27 orduniss 
 |-  ( Ord U. S -> U. U. S C_ U. S )
28 3 27 syl 
 |-  ( S C_ On -> U. U. S C_ U. S )
29 28 adantr 
 |-  ( ( S C_ On /\ -. U. S e. S ) -> U. U. S C_ U. S )
30 26 29 eqssd 
 |-  ( ( S C_ On /\ -. U. S e. S ) -> U. S = U. U. S )
31 30 adantr 
 |-  ( ( ( S C_ On /\ -. U. S e. S ) /\ S =/= (/) ) -> U. S = U. U. S )
32 df-lim 
 |-  ( Lim U. S <-> ( Ord U. S /\ U. S =/= (/) /\ U. S = U. U. S ) )
33 4 25 31 32 syl3anbrc 
 |-  ( ( ( S C_ On /\ -. U. S e. S ) /\ S =/= (/) ) -> Lim U. S )
34 33 an32s 
 |-  ( ( ( S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> Lim U. S )
35 34 3adantl1 
 |-  ( ( ( S e. T /\ S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> Lim U. S )
36 ssonuni 
 |-  ( S e. T -> ( S C_ On -> U. S e. On ) )
37 limeq 
 |-  ( y = U. S -> ( Lim y <-> Lim U. S ) )
38 fveq2 
 |-  ( y = U. S -> ( F ` y ) = ( F ` U. S ) )
39 iuneq1 
 |-  ( y = U. S -> U_ x e. y ( F ` x ) = U_ x e. U. S ( F ` x ) )
40 38 39 eqeq12d 
 |-  ( y = U. S -> ( ( F ` y ) = U_ x e. y ( F ` x ) <-> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) )
41 37 40 imbi12d 
 |-  ( y = U. S -> ( ( Lim y -> ( F ` y ) = U_ x e. y ( F ` x ) ) <-> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) ) )
42 41 1 vtoclg 
 |-  ( U. S e. On -> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) )
43 36 42 syl6 
 |-  ( S e. T -> ( S C_ On -> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) ) )
44 43 imp 
 |-  ( ( S e. T /\ S C_ On ) -> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) )
45 44 3adant3 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) )
46 45 adantr 
 |-  ( ( ( S e. T /\ S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> ( Lim U. S -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) ) )
47 35 46 mpd 
 |-  ( ( ( S e. T /\ S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> ( F ` U. S ) = U_ x e. U. S ( F ` x ) )
48 eluni2 
 |-  ( x e. U. S <-> E. y e. S x e. y )
49 ssel 
 |-  ( S C_ On -> ( y e. S -> y e. On ) )
50 49 anim1d 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> ( y e. On /\ x e. y ) ) )
51 onelon 
 |-  ( ( y e. On /\ x e. y ) -> x e. On )
52 50 51 syl6 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> x e. On ) )
53 49 adantrd 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> y e. On ) )
54 eloni 
 |-  ( y e. On -> Ord y )
55 49 54 syl6 
 |-  ( S C_ On -> ( y e. S -> Ord y ) )
56 ordelss 
 |-  ( ( Ord y /\ x e. y ) -> x C_ y )
57 56 a1i 
 |-  ( S C_ On -> ( ( Ord y /\ x e. y ) -> x C_ y ) )
58 55 57 syland 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> x C_ y ) )
59 52 53 58 3jcad 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> ( x e. On /\ y e. On /\ x C_ y ) ) )
60 59 2 syl6 
 |-  ( S C_ On -> ( ( y e. S /\ x e. y ) -> ( F ` x ) C_ ( F ` y ) ) )
61 60 expd 
 |-  ( S C_ On -> ( y e. S -> ( x e. y -> ( F ` x ) C_ ( F ` y ) ) ) )
62 61 reximdvai 
 |-  ( S C_ On -> ( E. y e. S x e. y -> E. y e. S ( F ` x ) C_ ( F ` y ) ) )
63 48 62 syl5bi 
 |-  ( S C_ On -> ( x e. U. S -> E. y e. S ( F ` x ) C_ ( F ` y ) ) )
64 ssiun 
 |-  ( E. y e. S ( F ` x ) C_ ( F ` y ) -> ( F ` x ) C_ U_ y e. S ( F ` y ) )
65 63 64 syl6 
 |-  ( S C_ On -> ( x e. U. S -> ( F ` x ) C_ U_ y e. S ( F ` y ) ) )
66 65 ralrimiv 
 |-  ( S C_ On -> A. x e. U. S ( F ` x ) C_ U_ y e. S ( F ` y ) )
67 iunss 
 |-  ( U_ x e. U. S ( F ` x ) C_ U_ y e. S ( F ` y ) <-> A. x e. U. S ( F ` x ) C_ U_ y e. S ( F ` y ) )
68 66 67 sylibr 
 |-  ( S C_ On -> U_ x e. U. S ( F ` x ) C_ U_ y e. S ( F ` y ) )
69 fveq2 
 |-  ( y = x -> ( F ` y ) = ( F ` x ) )
70 69 cbviunv 
 |-  U_ y e. S ( F ` y ) = U_ x e. S ( F ` x )
71 68 70 sseqtrdi 
 |-  ( S C_ On -> U_ x e. U. S ( F ` x ) C_ U_ x e. S ( F ` x ) )
72 71 3ad2ant2 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> U_ x e. U. S ( F ` x ) C_ U_ x e. S ( F ` x ) )
73 72 adantr 
 |-  ( ( ( S e. T /\ S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> U_ x e. U. S ( F ` x ) C_ U_ x e. S ( F ` x ) )
74 47 73 eqsstrd 
 |-  ( ( ( S e. T /\ S C_ On /\ S =/= (/) ) /\ -. U. S e. S ) -> ( F ` U. S ) C_ U_ x e. S ( F ` x ) )
75 74 ex 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( -. U. S e. S -> ( F ` U. S ) C_ U_ x e. S ( F ` x ) ) )
76 fveq2 
 |-  ( x = U. S -> ( F ` x ) = ( F ` U. S ) )
77 76 ssiun2s 
 |-  ( U. S e. S -> ( F ` U. S ) C_ U_ x e. S ( F ` x ) )
78 75 77 pm2.61d2 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( F ` U. S ) C_ U_ x e. S ( F ` x ) )
79 36 imp 
 |-  ( ( S e. T /\ S C_ On ) -> U. S e. On )
80 79 3adant3 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> U. S e. On )
81 8 3ad2ant2 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( x e. S -> x e. On ) )
82 81 6 jca2 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( x e. S -> ( x e. On /\ x C_ U. S ) ) )
83 sseq2 
 |-  ( y = U. S -> ( x C_ y <-> x C_ U. S ) )
84 83 anbi2d 
 |-  ( y = U. S -> ( ( x e. On /\ x C_ y ) <-> ( x e. On /\ x C_ U. S ) ) )
85 38 sseq2d 
 |-  ( y = U. S -> ( ( F ` x ) C_ ( F ` y ) <-> ( F ` x ) C_ ( F ` U. S ) ) )
86 84 85 imbi12d 
 |-  ( y = U. S -> ( ( ( x e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) ) <-> ( ( x e. On /\ x C_ U. S ) -> ( F ` x ) C_ ( F ` U. S ) ) ) )
87 2 3com12 
 |-  ( ( y e. On /\ x e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) )
88 87 3expib 
 |-  ( y e. On -> ( ( x e. On /\ x C_ y ) -> ( F ` x ) C_ ( F ` y ) ) )
89 86 88 vtoclga 
 |-  ( U. S e. On -> ( ( x e. On /\ x C_ U. S ) -> ( F ` x ) C_ ( F ` U. S ) ) )
90 80 82 89 sylsyld 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( x e. S -> ( F ` x ) C_ ( F ` U. S ) ) )
91 90 ralrimiv 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> A. x e. S ( F ` x ) C_ ( F ` U. S ) )
92 iunss 
 |-  ( U_ x e. S ( F ` x ) C_ ( F ` U. S ) <-> A. x e. S ( F ` x ) C_ ( F ` U. S ) )
93 91 92 sylibr 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> U_ x e. S ( F ` x ) C_ ( F ` U. S ) )
94 78 93 eqssd 
 |-  ( ( S e. T /\ S C_ On /\ S =/= (/) ) -> ( F ` U. S ) = U_ x e. S ( F ` x ) )