fpwwe2lem9

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) (Revised by AV, 20-Jul-2024)

	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$
	fpwwe2lem9.4	$⊢ φ \to X W R$
	fpwwe2lem9.6	$⊢ φ \to Y W S$
Assertion	fpwwe2lem9	$⊢ φ \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		fpwwe2lem9.4	$⊢ φ \to X W R$
5		fpwwe2lem9.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	fpwwe2lem8	$⊢ (φ \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	fpwwe2lem8	$⊢ (φ \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 fpwwe2lem9

Proof