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	biimtrid	\|- ( 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 ) )

Metamath Proof Explorer

Theorem onfununi

Proof