grudomon

Description: Each ordinal that is comparable with an element of the universe is in the universe. (Contributed by Mario Carneiro, 10-Jun-2013)

		Ref	Expression
	Assertion	grudomon	$⊢ (U \in Univ \land A \in On \land (B \in U \land A ≼ B)) \to A \in U$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = y \to (x ≼ B \leftrightarrow y ≼ B)$
2		eleq1	$⊢ x = y \to (x \in U \leftrightarrow y \in U)$
3	1 2	imbi12d	$⊢ x = y \to ((x ≼ B \to x \in U) \leftrightarrow (y ≼ B \to y \in U))$
4	3	imbi2d	$⊢ x = y \to (((U \in Univ \land B \in U) \to (x ≼ B \to x \in U)) \leftrightarrow ((U \in Univ \land B \in U) \to (y ≼ B \to y \in U)))$
5		breq1	$⊢ x = A \to (x ≼ B \leftrightarrow A ≼ B)$
6		eleq1	$⊢ x = A \to (x \in U \leftrightarrow A \in U)$
7	5 6	imbi12d	$⊢ x = A \to ((x ≼ B \to x \in U) \leftrightarrow (A ≼ B \to A \in U))$
8	7	imbi2d	$⊢ x = A \to (((U \in Univ \land B \in U) \to (x ≼ B \to x \in U)) \leftrightarrow ((U \in Univ \land B \in U) \to (A ≼ B \to A \in U)))$
9		r19.21v	$⊢ \forall y \in x ((U \in Univ \land B \in U) \to (y ≼ B \to y \in U)) \leftrightarrow ((U \in Univ \land B \in U) \to \forall y \in x (y ≼ B \to y \in U))$
10		simpl1	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to x \in On$
11		vex	$⊢ x \in V$
12		onelss	$⊢ x \in On \to (y \in x \to y \subseteq x)$
13	12	imp	$⊢ (x \in On \land y \in x) \to y \subseteq x$
14		ssdomg	$⊢ x \in V \to (y \subseteq x \to y ≼ x)$
15	11 13 14	mpsyl	$⊢ (x \in On \land y \in x) \to y ≼ x$
16	10 15	sylan	$⊢ (((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \land y \in x) \to y ≼ x$
17		simplr	$⊢ (((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \land y \in x) \to x ≼ B$
18		domtr	$⊢ (y ≼ x \land x ≼ B) \to y ≼ B$
19	16 17 18	syl2anc	$⊢ (((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \land y \in x) \to y ≼ B$
20		pm2.27	$⊢ y ≼ B \to ((y ≼ B \to y \in U) \to y \in U)$
21	19 20	syl	$⊢ (((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \land y \in x) \to ((y ≼ B \to y \in U) \to y \in U)$
22	21	ralimdva	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (\forall y \in x (y ≼ B \to y \in U) \to \forall y \in x y \in U)$
23		dfss3	$⊢ x \subseteq U \leftrightarrow \forall y \in x y \in U$
24		domeng	$⊢ B \in U \to (x ≼ B \leftrightarrow \exists y (x \approx y \land y \subseteq B))$
25	24	3ad2ant3	$⊢ (x \in On \land U \in Univ \land B \in U) \to (x ≼ B \leftrightarrow \exists y (x \approx y \land y \subseteq B))$
26	25	biimpa	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to \exists y (x \approx y \land y \subseteq B)$
27		simpl2	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to U \in Univ$
28		gruss	$⊢ (U \in Univ \land B \in U \land y \subseteq B) \to y \in U$
29	28	3expia	$⊢ (U \in Univ \land B \in U) \to (y \subseteq B \to y \in U)$
30	29	3adant1	$⊢ (x \in On \land U \in Univ \land B \in U) \to (y \subseteq B \to y \in U)$
31	30	adantr	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (y \subseteq B \to y \in U)$
32		ensym	$⊢ x \approx y \to y \approx x$
33	31 32	anim12d1	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to ((y \subseteq B \land x \approx y) \to (y \in U \land y \approx x))$
34	33	ancomsd	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to ((x \approx y \land y \subseteq B) \to (y \in U \land y \approx x))$
35	34	eximdv	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (\exists y (x \approx y \land y \subseteq B) \to \exists y (y \in U \land y \approx x))$
36		gruen	$⊢ (U \in Univ \land x \subseteq U \land (y \in U \land y \approx x)) \to x \in U$
37	36	3com23	$⊢ (U \in Univ \land (y \in U \land y \approx x) \land x \subseteq U) \to x \in U$
38	37	3exp	$⊢ U \in Univ \to ((y \in U \land y \approx x) \to (x \subseteq U \to x \in U))$
39	38	exlimdv	$⊢ U \in Univ \to (\exists y (y \in U \land y \approx x) \to (x \subseteq U \to x \in U))$
40	27 35 39	sylsyld	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (\exists y (x \approx y \land y \subseteq B) \to (x \subseteq U \to x \in U))$
41	26 40	mpd	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (x \subseteq U \to x \in U)$
42	23 41	syl5bir	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (\forall y \in x y \in U \to x \in U)$
43	22 42	syld	$⊢ ((x \in On \land U \in Univ \land B \in U) \land x ≼ B) \to (\forall y \in x (y ≼ B \to y \in U) \to x \in U)$
44	43	ex	$⊢ (x \in On \land U \in Univ \land B \in U) \to (x ≼ B \to (\forall y \in x (y ≼ B \to y \in U) \to x \in U))$
45	44	com23	$⊢ (x \in On \land U \in Univ \land B \in U) \to (\forall y \in x (y ≼ B \to y \in U) \to (x ≼ B \to x \in U))$
46	45	3expib	$⊢ x \in On \to ((U \in Univ \land B \in U) \to (\forall y \in x (y ≼ B \to y \in U) \to (x ≼ B \to x \in U)))$
47	46	a2d	$⊢ x \in On \to (((U \in Univ \land B \in U) \to \forall y \in x (y ≼ B \to y \in U)) \to ((U \in Univ \land B \in U) \to (x ≼ B \to x \in U)))$
48	9 47	syl5bi	$⊢ x \in On \to (\forall y \in x ((U \in Univ \land B \in U) \to (y ≼ B \to y \in U)) \to ((U \in Univ \land B \in U) \to (x ≼ B \to x \in U)))$
49	4 8 48	tfis3	$⊢ A \in On \to ((U \in Univ \land B \in U) \to (A ≼ B \to A \in U))$
50	49	com3l	$⊢ (U \in Univ \land B \in U) \to (A ≼ B \to (A \in On \to A \in U))$
51	50	impr	$⊢ (U \in Univ \land (B \in U \land A ≼ B)) \to (A \in On \to A \in U)$
52	51	3impia	$⊢ (U \in Univ \land (B \in U \land A ≼ B) \land A \in On) \to A \in U$
53	52	3com23	$⊢ (U \in Univ \land A \in On \land (B \in U \land A ≼ B)) \to A \in U$

Metamath Proof Explorer

Theorem grudomon

Proof