fpwwe2lem10

Description: Lemma for fpwwe2 . Given two well-orders <. X , R >. and <. Y , S >. of parts of A , one is an initial segment of the other. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Hypotheses	fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
	fpwwe2.2	$⊢ φ \to A \in V$
	fpwwe2.3	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
	fpwwe2lem10.4	$⊢ φ \to X W R$
	fpwwe2lem10.6	$⊢ φ \to Y W S$
Assertion	fpwwe2lem10	$⊢ φ \to ((X \subseteq Y \land R = S \cap (Y \times X)) \lor (Y \subseteq X \land S = R \cap (X \times Y)))$

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
2		fpwwe2.2	$⊢ φ \to A \in V$
3		fpwwe2.3	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
4		fpwwe2lem10.4	$⊢ φ \to X W R$
5		fpwwe2lem10.6	$⊢ φ \to Y W S$
6		eqid	$⊢ OrdIso (R, X) = OrdIso (R, X)$
7	6	oicl	$⊢ Ord dom OrdIso (R, X)$
8		eqid	$⊢ OrdIso (S, Y) = OrdIso (S, Y)$
9	8	oicl	$⊢ Ord dom OrdIso (S, Y)$
10		ordtri2or2	$⊢ (Ord dom OrdIso (R, X) \land Ord dom OrdIso (S, Y)) \to (dom OrdIso (R, X) \subseteq dom OrdIso (S, Y) \lor dom OrdIso (S, Y) \subseteq dom OrdIso (R, X))$
11	7 9 10	mp2an	$⊢ (dom OrdIso (R, X) \subseteq dom OrdIso (S, Y) \lor dom OrdIso (S, Y) \subseteq dom OrdIso (R, X))$
12	2	adantr	$⊢ (φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \to A \in V$
13	3	adantlr	$⊢ ((φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
14	4	adantr	$⊢ (φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \to X W R$
15	5	adantr	$⊢ (φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \to Y W S$
16		simpr	$⊢ (φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \to dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)$
17	1 12 13 14 15 6 8 16	fpwwe2lem9	$⊢ (φ \land dom OrdIso (R, X) \subseteq dom OrdIso (S, Y)) \to (X \subseteq Y \land R = S \cap (Y \times X))$
18	17	ex	$⊢ φ \to (dom OrdIso (R, X) \subseteq dom OrdIso (S, Y) \to (X \subseteq Y \land R = S \cap (Y \times X)))$
19	2	adantr	$⊢ (φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to A \in V$
20	3	adantlr	$⊢ ((φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
21	5	adantr	$⊢ (φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to Y W S$
22	4	adantr	$⊢ (φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to X W R$
23		simpr	$⊢ (φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)$
24	1 19 20 21 22 8 6 23	fpwwe2lem9	$⊢ (φ \land dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to (Y \subseteq X \land S = R \cap (X \times Y))$
25	24	ex	$⊢ φ \to (dom OrdIso (S, Y) \subseteq dom OrdIso (R, X) \to (Y \subseteq X \land S = R \cap (X \times Y)))$
26	18 25	orim12d	$⊢ φ \to ((dom OrdIso (R, X) \subseteq dom OrdIso (S, Y) \lor dom OrdIso (S, Y) \subseteq dom OrdIso (R, X)) \to ((X \subseteq Y \land R = S \cap (Y \times X)) \lor (Y \subseteq X \land S = R \cap (X \times Y))))$
27	11 26	mpi	$⊢ φ \to ((X \subseteq Y \land R = S \cap (Y \times X)) \lor (Y \subseteq X \land S = R \cap (X \times Y)))$

Metamath Proof Explorer

Theorem fpwwe2lem10

Proof