onfrALTlem2

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	onfrALTlem2	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \exists y \in a a \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in (a \cap y)$
2	1	2a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in (a \cap y)))$
3		inss2	$⊢ a \cap y \subseteq y$
4	3	sseli	$⊢ z \in (a \cap y) \to z \in y$
5	2 4	syl8	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in y))$
6		inss1	$⊢ a \cap y \subseteq a$
7	6	sseli	$⊢ z \in (a \cap y) \to z \in a$
8	2 7	syl8	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in a))$
9		simpl	$⊢ (a \subseteq On \land a \neq \emptyset) \to a \subseteq On$
10		simpl	$⊢ (x \in a \land \neg a \cap x = \emptyset) \to x \in a$
11		ssel	$⊢ a \subseteq On \to (x \in a \to x \in On)$
12	9 10 11	syl2im	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to x \in On)$
13		eloni	$⊢ x \in On \to Ord x$
14	12 13	syl6	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to Ord x)$
15		ordtr	$⊢ Ord x \to Tr x$
16	14 15	syl6	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to Tr x)$
17		simpll	$⊢ ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to y \in (a \cap x)$
18	17	2a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to y \in (a \cap x)))$
19		inss2	$⊢ a \cap x \subseteq x$
20	19	sseli	$⊢ y \in (a \cap x) \to y \in x$
21	18 20	syl8	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to y \in x))$
22		trel	$⊢ Tr x \to ((z \in y \land y \in x) \to z \in x)$
23	22	expcomd	$⊢ Tr x \to (y \in x \to (z \in y \to z \in x))$
24	16 21 5 23	ee233	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in x))$
25		elin	$⊢ z \in (a \cap x) \leftrightarrow (z \in a \land z \in x)$
26	25	simplbi2	$⊢ z \in a \to (z \in x \to z \in (a \cap x))$
27	8 24 26	ee33	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in (a \cap x)))$
28		elin	$⊢ z \in ((a \cap x) \cap y) \leftrightarrow (z \in (a \cap x) \land z \in y)$
29	28	simplbi2com	$⊢ z \in y \to (z \in (a \cap x) \to z \in ((a \cap x) \cap y))$
30	5 27 29	ee33	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in ((a \cap x) \cap y)))$
31	30	exp4a	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (z \in (a \cap y) \to z \in ((a \cap x) \cap y))))$
32	31	ggen31	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to \forall z (z \in (a \cap y) \to z \in ((a \cap x) \cap y))))$
33		df-ss	$⊢ a \cap y \subseteq (a \cap x) \cap y \leftrightarrow \forall z (z \in (a \cap y) \to z \in ((a \cap x) \cap y))$
34	33	biimpri	$⊢ \forall z (z \in (a \cap y) \to z \in ((a \cap x) \cap y)) \to a \cap y \subseteq (a \cap x) \cap y$
35	32 34	syl8	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to a \cap y \subseteq (a \cap x) \cap y))$
36		simpr	$⊢ (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (a \cap x) \cap y = \emptyset$
37	36	2a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (a \cap x) \cap y = \emptyset))$
38		sseq0	$⊢ (a \cap y \subseteq (a \cap x) \cap y \land (a \cap x) \cap y = \emptyset) \to a \cap y = \emptyset$
39	38	ex	$⊢ a \cap y \subseteq (a \cap x) \cap y \to ((a \cap x) \cap y = \emptyset \to a \cap y = \emptyset)$
40	35 37 39	ee33	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to a \cap y = \emptyset))$
41		simpl	$⊢ (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in (a \cap x)$
42	41	2a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in (a \cap x)))$
43		inss1	$⊢ a \cap x \subseteq a$
44	43	sseli	$⊢ y \in (a \cap x) \to y \in a$
45	42 44	syl8	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in a))$
46		pm3.21	$⊢ a \cap y = \emptyset \to (y \in a \to (y \in a \land a \cap y = \emptyset))$
47	40 45 46	ee33	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (y \in a \land a \cap y = \emptyset)))$
48	47	alrimdv	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \forall y ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (y \in a \land a \cap y = \emptyset)))$
49		onfrALTlem3	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset)$
50		df-rex	$⊢ \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset \leftrightarrow \exists y (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset)$
51	49 50	imbitrdi	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \exists y (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset))$
52		exim	$⊢ \forall y ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (y \in a \land a \cap y = \emptyset)) \to (\exists y (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to \exists y (y \in a \land a \cap y = \emptyset))$
53	48 51 52	syl6c	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \exists y (y \in a \land a \cap y = \emptyset))$
54		df-rex	$⊢ \exists y \in a a \cap y = \emptyset \leftrightarrow \exists y (y \in a \land a \cap y = \emptyset)$
55	53 54	imbitrrdi	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \exists y \in a a \cap y = \emptyset)$

Metamath Proof Explorer

Theorem onfrALTlem2

Proof