onfrALTlem2VD

Description: Virtual deduction proof of onfrALTlem2 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem2 is onfrALTlem2VD without virtual deductions and was automatically derived from onfrALTlem2VD .

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

Proof

Step	Hyp	Ref	Expression
1		idn3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)))$
2		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)$
3	1 2	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in (a \cap y))$
4		inss2	$⊢ a \cap y \subseteq y$
5	4	sseli	$⊢ z \in (a \cap y) \to z \in y$
6	3 5	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in y)$
7		inss1	$⊢ a \cap y \subseteq a$
8	7	sseli	$⊢ z \in (a \cap y) \to z \in a$
9	3 8	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in a)$
10		idn2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to (x \in a \land \neg a \cap x = \emptyset))$
11		simpl	$⊢ (x \in a \land \neg a \cap x = \emptyset) \to x \in a$
12	10 11	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to x \in a)$
13		idn1	$⊢ ((a \subseteq On \land a \neq \emptyset) \to (a \subseteq On \land a \neq \emptyset))$
14		simpl	$⊢ (a \subseteq On \land a \neq \emptyset) \to a \subseteq On$
15	13 14	e1a	$⊢ ((a \subseteq On \land a \neq \emptyset) \to a \subseteq On)$
16		ssel	$⊢ a \subseteq On \to (x \in a \to x \in On)$
17	16	com12	$⊢ x \in a \to (a \subseteq On \to x \in On)$
18	12 15 17	e21	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to x \in On)$
19		eloni	$⊢ x \in On \to Ord x$
20	18 19	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to Ord x)$
21		ordtr	$⊢ Ord x \to Tr x$
22	20 21	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to Tr x)$
23		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)$
24	1 23	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to y \in (a \cap x))$
25		inss2	$⊢ a \cap x \subseteq x$
26	25	sseli	$⊢ y \in (a \cap x) \to y \in x$
27	24 26	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to y \in x)$
28		trel	$⊢ Tr x \to ((z \in y \land y \in x) \to z \in x)$
29	28	expcomd	$⊢ Tr x \to (y \in x \to (z \in y \to z \in x))$
30	22 27 6 29	e233	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in x)$
31		elin	$⊢ z \in (a \cap x) \leftrightarrow (z \in a \land z \in x)$
32	31	simplbi2	$⊢ z \in a \to (z \in x \to z \in (a \cap x))$
33	9 30 32	e33	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \land z \in (a \cap y)) \to z \in (a \cap x))$
34		elin	$⊢ z \in ((a \cap x) \cap y) \leftrightarrow (z \in (a \cap x) \land z \in y)$
35	34	simplbi2com	$⊢ z \in y \to (z \in (a \cap x) \to z \in ((a \cap x) \cap y))$
36	6 33 35	e33	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), ((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))$
37	36	in3an	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (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)))$
38	37	gen31	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (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)))$
39		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))$
40	39	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$
41	38 40	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to a \cap y \subseteq (a \cap x) \cap y)$
42		idn3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset))$
43		simpr	$⊢ (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (a \cap x) \cap y = \emptyset$
44	42 43	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (a \cap x) \cap y = \emptyset)$
45		sseq0	$⊢ (a \cap y \subseteq (a \cap x) \cap y \land (a \cap x) \cap y = \emptyset) \to a \cap y = \emptyset$
46	45	ex	$⊢ a \cap y \subseteq (a \cap x) \cap y \to ((a \cap x) \cap y = \emptyset \to a \cap y = \emptyset)$
47	41 44 46	e33	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to a \cap y = \emptyset)$
48		simpl	$⊢ (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in (a \cap x)$
49	42 48	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in (a \cap x))$
50		inss1	$⊢ a \cap x \subseteq a$
51	50	sseli	$⊢ y \in (a \cap x) \to y \in a$
52	49 51	e3	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to y \in a)$
53		pm3.21	$⊢ a \cap y = \emptyset \to (y \in a \to (y \in a \land a \cap y = \emptyset))$
54	47 52 53	e33	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset), (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset) \to (y \in a \land a \cap y = \emptyset))$
55	54	in3	$⊢ ((a \subseteq On \land a \neq \emptyset), (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)))$
56	55	gen21	$⊢ ((a \subseteq On \land a \neq \emptyset), (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)))$
57		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))$
58	56 57	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \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)))$
59		onfrALTlem3VD	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset)$
60		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)$
61	60	biimpi	$⊢ \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset \to \exists y (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset)$
62	59 61	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to \exists y (y \in (a \cap x) \land (a \cap x) \cap y = \emptyset))$
63		id	$⊢ (\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)) \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))$
64	58 62 63	e22	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to \exists y (y \in a \land a \cap y = \emptyset))$
65		df-rex	$⊢ \exists y \in a a \cap y = \emptyset \leftrightarrow \exists y (y \in a \land a \cap y = \emptyset)$
66	65	biimpri	$⊢ \exists y (y \in a \land a \cap y = \emptyset) \to \exists y \in a a \cap y = \emptyset$
67	64 66	e2	$⊢ ((a \subseteq On \land a \neq \emptyset), (x \in a \land \neg a \cap x = \emptyset) \to \exists y \in a a \cap y = \emptyset)$

1::	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ).
2:1:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i y ) ).
3:2:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. a ).
4::	\|- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
5::	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
6:5:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
7:4:	\|- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
8:6,7:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
9:8:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
10:9:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Tr x ).
11:1:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. ( a i^i x ) ).
12:11:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. y e. x ).
13:2:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. y ).
14:10,12,13:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. x ).
15:3,14:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( a i^i x ) ).
16:13,15:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) /\ z e. ( a i^i y ) ) ->. z e. ( ( a i^i x ) i^i y ) ).
17:16:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
18:17:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. A. z ( z e. ( a i^i y ) -> z e. ( ( a i^i x ) i^i y ) ) ).
19:18:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) C_ ( ( a i^i x ) i^i y ) ).
20::	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
21:20:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( ( a i^i x ) i^i y ) = (/) ).
22:19,21:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( a i^i y ) = (/) ).
23:20:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. ( a i^i x ) ).
24:23:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. y e. a ).
25:22,24:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) , ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ->. ( y e. a /\ ( a i^i y ) = (/) ) ).
26:25:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
27:26:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. y ( ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> ( y e. a /\ ( a i^i y ) = (/) ) ) ).
28:27:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) -> E. y ( y e. a /\ ( a i^i y ) = (/) ) ) ).
29::	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ).
30:29:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) ).
31:28,30:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y ( y e. a /\ ( a i^i y ) = (/) ) ).
qed:31:	\|- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. a ( a i^i y ) = (/) ).

Metamath Proof Explorer

Theorem onfrALTlem2VD

Proof