smogt

Description: A strictly monotone ordinal function is greater than or equal to its argument. Exercise 1 in TakeutiZaring p. 50. (Contributed by Andrew Salmon, 23-Nov-2011) (Revised by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Assertion	smogt	$⊢ (F Fn A \land Smo F \land C \in A) \to C \subseteq F (C)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ x = C \to x = C$
2		fveq2	$⊢ x = C \to F (x) = F (C)$
3	1 2	sseq12d	$⊢ x = C \to (x \subseteq F (x) \leftrightarrow C \subseteq F (C))$
4	3	imbi2d	$⊢ x = C \to (((F Fn A \land Smo F) \to x \subseteq F (x)) \leftrightarrow ((F Fn A \land Smo F) \to C \subseteq F (C)))$
5		smodm2	$⊢ (F Fn A \land Smo F) \to Ord A$
6	5	3adant3	$⊢ (F Fn A \land Smo F \land x \in A) \to Ord A$
7		simp3	$⊢ (F Fn A \land Smo F \land x \in A) \to x \in A$
8		ordelord	$⊢ (Ord A \land x \in A) \to Ord x$
9	6 7 8	syl2anc	$⊢ (F Fn A \land Smo F \land x \in A) \to Ord x$
10		vex	$⊢ x \in V$
11	10	elon	$⊢ x \in On \leftrightarrow Ord x$
12	9 11	sylibr	$⊢ (F Fn A \land Smo F \land x \in A) \to x \in On$
13		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
14	13	3anbi3d	$⊢ x = y \to ((F Fn A \land Smo F \land x \in A) \leftrightarrow (F Fn A \land Smo F \land y \in A))$
15		id	$⊢ x = y \to x = y$
16		fveq2	$⊢ x = y \to F (x) = F (y)$
17	15 16	sseq12d	$⊢ x = y \to (x \subseteq F (x) \leftrightarrow y \subseteq F (y))$
18	14 17	imbi12d	$⊢ x = y \to (((F Fn A \land Smo F \land x \in A) \to x \subseteq F (x)) \leftrightarrow ((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)))$
19		simpl1	$⊢ ((F Fn A \land Smo F \land x \in A) \land y \in x) \to F Fn A$
20		simpl2	$⊢ ((F Fn A \land Smo F \land x \in A) \land y \in x) \to Smo F$
21		ordtr1	$⊢ Ord A \to ((y \in x \land x \in A) \to y \in A)$
22	21	expcomd	$⊢ Ord A \to (x \in A \to (y \in x \to y \in A))$
23	6 7 22	sylc	$⊢ (F Fn A \land Smo F \land x \in A) \to (y \in x \to y \in A)$
24	23	imp	$⊢ ((F Fn A \land Smo F \land x \in A) \land y \in x) \to y \in A$
25		pm2.27	$⊢ (F Fn A \land Smo F \land y \in A) \to (((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)) \to y \subseteq F (y))$
26	19 20 24 25	syl3anc	$⊢ ((F Fn A \land Smo F \land x \in A) \land y \in x) \to (((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)) \to y \subseteq F (y))$
27	26	ralimdva	$⊢ (F Fn A \land Smo F \land x \in A) \to (\forall y \in x ((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)) \to \forall y \in x y \subseteq F (y))$
28	5	3adant3	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to Ord A$
29		simp31	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to x \in A$
30	28 29 8	syl2anc	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to Ord x$
31		simp32	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to y \in x$
32		ordelord	$⊢ (Ord x \land y \in x) \to Ord y$
33	30 31 32	syl2anc	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to Ord y$
34		smofvon2	$⊢ Smo F \to F (x) \in On$
35	34	3ad2ant2	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to F (x) \in On$
36		eloni	$⊢ F (x) \in On \to Ord F (x)$
37	35 36	syl	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to Ord F (x)$
38		simp33	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to y \subseteq F (y)$
39		smoel2	$⊢ ((F Fn A \land Smo F) \land (x \in A \land y \in x)) \to F (y) \in F (x)$
40	39	3adantr3	$⊢ ((F Fn A \land Smo F) \land (x \in A \land y \in x \land y \subseteq F (y))) \to F (y) \in F (x)$
41	40	3impa	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to F (y) \in F (x)$
42		ordtr2	$⊢ (Ord y \land Ord F (x)) \to ((y \subseteq F (y) \land F (y) \in F (x)) \to y \in F (x))$
43	42	imp	$⊢ ((Ord y \land Ord F (x)) \land (y \subseteq F (y) \land F (y) \in F (x))) \to y \in F (x)$
44	33 37 38 41 43	syl22anc	$⊢ (F Fn A \land Smo F \land (x \in A \land y \in x \land y \subseteq F (y))) \to y \in F (x)$
45	44	3expia	$⊢ (F Fn A \land Smo F) \to ((x \in A \land y \in x \land y \subseteq F (y)) \to y \in F (x))$
46	45	3expd	$⊢ (F Fn A \land Smo F) \to (x \in A \to (y \in x \to (y \subseteq F (y) \to y \in F (x))))$
47	46	3impia	$⊢ (F Fn A \land Smo F \land x \in A) \to (y \in x \to (y \subseteq F (y) \to y \in F (x)))$
48	47	imp	$⊢ ((F Fn A \land Smo F \land x \in A) \land y \in x) \to (y \subseteq F (y) \to y \in F (x))$
49	48	ralimdva	$⊢ (F Fn A \land Smo F \land x \in A) \to (\forall y \in x y \subseteq F (y) \to \forall y \in x y \in F (x))$
50		dfss3	$⊢ x \subseteq F (x) \leftrightarrow \forall y \in x y \in F (x)$
51	49 50	syl6ibr	$⊢ (F Fn A \land Smo F \land x \in A) \to (\forall y \in x y \subseteq F (y) \to x \subseteq F (x))$
52	27 51	syldc	$⊢ \forall y \in x ((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)) \to ((F Fn A \land Smo F \land x \in A) \to x \subseteq F (x))$
53	52	a1i	$⊢ x \in On \to (\forall y \in x ((F Fn A \land Smo F \land y \in A) \to y \subseteq F (y)) \to ((F Fn A \land Smo F \land x \in A) \to x \subseteq F (x)))$
54	18 53	tfis2	$⊢ x \in On \to ((F Fn A \land Smo F \land x \in A) \to x \subseteq F (x))$
55	12 54	mpcom	$⊢ (F Fn A \land Smo F \land x \in A) \to x \subseteq F (x)$
56	55	3expia	$⊢ (F Fn A \land Smo F) \to (x \in A \to x \subseteq F (x))$
57	56	com12	$⊢ x \in A \to ((F Fn A \land Smo F) \to x \subseteq F (x))$
58	4 57	vtoclga	$⊢ C \in A \to ((F Fn A \land Smo F) \to C \subseteq F (C))$
59	58	com12	$⊢ (F Fn A \land Smo F) \to (C \in A \to C \subseteq F (C))$
60	59	3impia	$⊢ (F Fn A \land Smo F \land C \in A) \to C \subseteq F (C)$

Metamath Proof Explorer

Theorem smogt

Proof