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 \to F (y) = ⋃_{x \in y} F (x)$
	onfununi.2	$⊢ (x \in On \land y \in On \land x \subseteq y) \to F (x) \subseteq F (y)$
Assertion	onfununi	$⊢ (S \in T \land S \subseteq On \land S \neq \emptyset) \to F (⋃ S) = ⋃_{x \in S} F (x)$

Proof

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

Metamath Proof Explorer

Theorem onfununi

Proof