onfrALTlem3

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

		Ref	Expression
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		ssid	$⊢ a \cap x \subseteq a \cap x$
2		simpr	$⊢ (x \in a \land \neg a \cap x = \emptyset) \to \neg a \cap x = \emptyset$
3	2	a1i	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \neg a \cap x = \emptyset)$
4		df-ne	$⊢ a \cap x \neq \emptyset \leftrightarrow \neg a \cap x = \emptyset$
5	3 4	syl6ibr	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to a \cap x \neq \emptyset)$
6		pm3.2	$⊢ a \cap x \subseteq a \cap x \to (a \cap x \neq \emptyset \to (a \cap x \subseteq a \cap x \land a \cap x \neq \emptyset))$
7	1 5 6	mpsylsyld	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to (a \cap x \subseteq a \cap x \land a \cap x \neq \emptyset))$
8		vex	$⊢ x \in V$
9	8	inex2	$⊢ a \cap x \in V$
10		inss2	$⊢ a \cap x \subseteq x$
11		simpl	$⊢ (a \subseteq On \land a \neq \emptyset) \to a \subseteq On$
12		simpl	$⊢ (x \in a \land \neg a \cap x = \emptyset) \to x \in a$
13		ssel	$⊢ a \subseteq On \to (x \in a \to x \in On)$
14	11 12 13	syl2im	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to x \in On)$
15		eloni	$⊢ x \in On \to Ord x$
16	14 15	syl6	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to Ord x)$
17		ordwe	$⊢ Ord x \to E We x$
18	16 17	syl6	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to E We x)$
19		wess	$⊢ a \cap x \subseteq x \to (E We x \to E We (a \cap x))$
20	10 18 19	mpsylsyld	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to E We (a \cap x))$
21		wefr	$⊢ E We (a \cap x) \to E Fr (a \cap x)$
22	20 21	syl6	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to E Fr (a \cap x))$
23		dfepfr	$⊢ E Fr (a \cap x) \leftrightarrow \forall b ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset)$
24	22 23	syl6ib	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \forall b ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset))$
25		spsbc	$⊢ a \cap x \in V \to (\forall b ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset) \to \underset{˙}{[} (a \cap x) / b \underset{˙}{]} ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset))$
26	9 24 25	mpsylsyld	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to \underset{˙}{[} (a \cap x) / b \underset{˙}{]} ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset))$
27		onfrALTlem5	$⊢ \underset{˙}{[} (a \cap x) / b \underset{˙}{]} ((b \subseteq a \cap x \land b \neq \emptyset) \to \exists y \in b b \cap y = \emptyset) \leftrightarrow ((a \cap x \subseteq a \cap x \land a \cap x \neq \emptyset) \to \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset)$
28	26 27	syl6ib	$⊢ (a \subseteq On \land a \neq \emptyset) \to ((x \in a \land \neg a \cap x = \emptyset) \to ((a \cap x \subseteq a \cap x \land a \cap x \neq \emptyset) \to \exists y \in (a \cap x) (a \cap x) \cap y = \emptyset))$
29	7 28	mpdd	$⊢ (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)$

Metamath Proof Explorer

Theorem onfrALTlem3

Proof