fpwwe2lem8

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. (The O C_ P hypothesis is in order to break the symmetry of X and Y .) (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (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$
	fpwwe2lem8.x	$⊢ φ \to X W R$
	fpwwe2lem8.y	$⊢ φ \to Y W S$
	fpwwe2lem8.m	$⊢ M = OrdIso (R, X)$
	fpwwe2lem8.n	$⊢ N = OrdIso (S, Y)$
	fpwwe2lem8.s	$⊢ φ \to dom M \subseteq dom N$
Assertion	fpwwe2lem8	$⊢ φ \to (X \subseteq Y \land R = S \cap (Y \times X))$

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		fpwwe2lem8.x	$⊢ φ \to X W R$
5		fpwwe2lem8.y	$⊢ φ \to Y W S$
6		fpwwe2lem8.m	$⊢ M = OrdIso (R, X)$
7		fpwwe2lem8.n	$⊢ N = OrdIso (S, Y)$
8		fpwwe2lem8.s	$⊢ φ \to dom M \subseteq dom N$
9	1	relopabiv	$⊢ Rel W$
10	9	brrelex1i	$⊢ X W R \to X \in V$
11	4 10	syl	$⊢ φ \to X \in V$
12	1 2	fpwwe2lem2	$⊢ φ \to (X W R \leftrightarrow ((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)))$
13	4 12	mpbid	$⊢ φ \to ((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))$
14	13	simprld	$⊢ φ \to R We X$
15	6	oiiso	$⊢ (X \in V \land R We X) \to M {Isom}_{E, R} (dom M, X)$
16	11 14 15	syl2anc	$⊢ φ \to M {Isom}_{E, R} (dom M, X)$
17		isof1o	$⊢ M {Isom}_{E, R} (dom M, X) \to M : dom M \underset{1-1 onto}{⟶} X$
18		f1ofo	$⊢ M : dom M \underset{1-1 onto}{⟶} X \to M : dom M \underset{onto}{⟶} X$
19		forn	$⊢ M : dom M \underset{onto}{⟶} X \to ran M = X$
20	16 17 18 19	4syl	$⊢ φ \to ran M = X$
21	1 2 3 4 5 6 7 8	fpwwe2lem7	$⊢ φ \to M = {N ↾}_{dom M}$
22	21	rneqd	$⊢ φ \to ran M = ran ({N ↾}_{dom M})$
23	20 22	eqtr3d	$⊢ φ \to X = ran ({N ↾}_{dom M})$
24		df-ima	$⊢ N [dom M] = ran ({N ↾}_{dom M})$
25	23 24	eqtr4di	$⊢ φ \to X = N [dom M]$
26		imassrn	$⊢ N [dom M] \subseteq ran N$
27	9	brrelex1i	$⊢ Y W S \to Y \in V$
28	5 27	syl	$⊢ φ \to Y \in V$
29	1 2	fpwwe2lem2	$⊢ φ \to (Y W S \leftrightarrow ((Y \subseteq A \land S \subseteq Y \times Y) \land (S We Y \land \forall y \in Y \underset{˙}{[} S^{-1} [\{y\}] / u \underset{˙}{]} u F (S \cap (u \times u)) = y)))$
30	5 29	mpbid	$⊢ φ \to ((Y \subseteq A \land S \subseteq Y \times Y) \land (S We Y \land \forall y \in Y \underset{˙}{[} S^{-1} [\{y\}] / u \underset{˙}{]} u F (S \cap (u \times u)) = y))$
31	30	simprld	$⊢ φ \to S We Y$
32	7	oiiso	$⊢ (Y \in V \land S We Y) \to N {Isom}_{E, S} (dom N, Y)$
33	28 31 32	syl2anc	$⊢ φ \to N {Isom}_{E, S} (dom N, Y)$
34		isof1o	$⊢ N {Isom}_{E, S} (dom N, Y) \to N : dom N \underset{1-1 onto}{⟶} Y$
35		f1ofo	$⊢ N : dom N \underset{1-1 onto}{⟶} Y \to N : dom N \underset{onto}{⟶} Y$
36		forn	$⊢ N : dom N \underset{onto}{⟶} Y \to ran N = Y$
37	33 34 35 36	4syl	$⊢ φ \to ran N = Y$
38	26 37	sseqtrid	$⊢ φ \to N [dom M] \subseteq Y$
39	25 38	eqsstrd	$⊢ φ \to X \subseteq Y$
40	13	simplrd	$⊢ φ \to R \subseteq X \times X$
41		relxp	$⊢ Rel (X \times X)$
42		relss	$⊢ R \subseteq X \times X \to (Rel (X \times X) \to Rel R)$
43	40 41 42	mpisyl	$⊢ φ \to Rel R$
44		relinxp	$⊢ Rel (S \cap (Y \times X))$
45	43 44	jctir	$⊢ φ \to (Rel R \land Rel (S \cap (Y \times X)))$
46	40	ssbrd	$⊢ φ \to (x R y \to x (X \times X) y)$
47		brxp	$⊢ x (X \times X) y \leftrightarrow (x \in X \land y \in X)$
48	46 47	imbitrdi	$⊢ φ \to (x R y \to (x \in X \land y \in X))$
49		brinxp2	$⊢ x (S \cap (Y \times X)) y \leftrightarrow ((x \in Y \land y \in X) \land x S y)$
50		isocnv	$⊢ N {Isom}_{E, S} (dom N, Y) \to N^{-1} {Isom}_{S, E} (Y, dom N)$
51	33 50	syl	$⊢ φ \to N^{-1} {Isom}_{S, E} (Y, dom N)$
52	51	adantr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} {Isom}_{S, E} (Y, dom N)$
53		isof1o	$⊢ N^{-1} {Isom}_{S, E} (Y, dom N) \to N^{-1} : Y \underset{1-1 onto}{⟶} dom N$
54		f1ofn	$⊢ N^{-1} : Y \underset{1-1 onto}{⟶} dom N \to N^{-1} Fn Y$
55	52 53 54	3syl	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} Fn Y$
56		simprll	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to x \in Y$
57		simprr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to x S y$
58	39	adantr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to X \subseteq Y$
59		simprlr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to y \in X$
60	58 59	sseldd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to y \in Y$
61		isorel	$⊢ (N^{-1} {Isom}_{S, E} (Y, dom N) \land (x \in Y \land y \in Y)) \to (x S y \leftrightarrow N^{-1} (x) E N^{-1} (y))$
62	52 56 60 61	syl12anc	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to (x S y \leftrightarrow N^{-1} (x) E N^{-1} (y))$
63	57 62	mpbid	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} (x) E N^{-1} (y)$
64		fvex	$⊢ N^{-1} (y) \in V$
65	64	epeli	$⊢ N^{-1} (x) E N^{-1} (y) \leftrightarrow N^{-1} (x) \in N^{-1} (y)$
66	63 65	sylib	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} (x) \in N^{-1} (y)$
67	21	adantr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M = {N ↾}_{dom M}$
68	67	cnveqd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} = {({N ↾}_{dom M})}^{-1}$
69		fnfun	$⊢ N^{-1} Fn Y \to Fun N^{-1}$
70		funcnvres	$⊢ Fun N^{-1} \to {({N ↾}_{dom M})}^{-1} = {N^{-1} ↾}_{N [dom M]}$
71	55 69 70	3syl	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to {({N ↾}_{dom M})}^{-1} = {N^{-1} ↾}_{N [dom M]}$
72	68 71	eqtrd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} = {N^{-1} ↾}_{N [dom M]}$
73	72	fveq1d	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} (y) = ({N^{-1} ↾}_{N [dom M]}) (y)$
74	25	adantr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to X = N [dom M]$
75	59 74	eleqtrd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to y \in N [dom M]$
76	75	fvresd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to ({N^{-1} ↾}_{N [dom M]}) (y) = N^{-1} (y)$
77	73 76	eqtrd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} (y) = N^{-1} (y)$
78		isocnv	$⊢ M {Isom}_{E, R} (dom M, X) \to M^{-1} {Isom}_{R, E} (X, dom M)$
79		isof1o	$⊢ M^{-1} {Isom}_{R, E} (X, dom M) \to M^{-1} : X \underset{1-1 onto}{⟶} dom M$
80		f1of	$⊢ M^{-1} : X \underset{1-1 onto}{⟶} dom M \to M^{-1} : X ⟶ dom M$
81	16 78 79 80	4syl	$⊢ φ \to M^{-1} : X ⟶ dom M$
82	81	adantr	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} : X ⟶ dom M$
83	82 59	ffvelcdmd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to M^{-1} (y) \in dom M$
84	77 83	eqeltrrd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} (y) \in dom M$
85	6	oicl	$⊢ Ord dom M$
86		ordtr1	$⊢ Ord dom M \to ((N^{-1} (x) \in N^{-1} (y) \land N^{-1} (y) \in dom M) \to N^{-1} (x) \in dom M)$
87	85 86	ax-mp	$⊢ (N^{-1} (x) \in N^{-1} (y) \land N^{-1} (y) \in dom M) \to N^{-1} (x) \in dom M$
88	66 84 87	syl2anc	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to N^{-1} (x) \in dom M$
89	55 56 88	elpreimad	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to x \in {N^{-1}}^{-1} [dom M]$
90		imacnvcnv	$⊢ {N^{-1}}^{-1} [dom M] = N [dom M]$
91	74 90	eqtr4di	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to X = {N^{-1}}^{-1} [dom M]$
92	89 91	eleqtrrd	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to x \in X$
93	92 59	jca	$⊢ (φ \land ((x \in Y \land y \in X) \land x S y)) \to (x \in X \land y \in X)$
94	93	ex	$⊢ φ \to (((x \in Y \land y \in X) \land x S y) \to (x \in X \land y \in X))$
95	49 94	biimtrid	$⊢ φ \to (x (S \cap (Y \times X)) y \to (x \in X \land y \in X))$
96	21	adantr	$⊢ (φ \land (x \in X \land y \in X)) \to M = {N ↾}_{dom M}$
97	96	cnveqd	$⊢ (φ \land (x \in X \land y \in X)) \to M^{-1} = {({N ↾}_{dom M})}^{-1}$
98	97	fveq1d	$⊢ (φ \land (x \in X \land y \in X)) \to M^{-1} (x) = {({N ↾}_{dom M})}^{-1} (x)$
99	97	fveq1d	$⊢ (φ \land (x \in X \land y \in X)) \to M^{-1} (y) = {({N ↾}_{dom M})}^{-1} (y)$
100	98 99	breq12d	$⊢ (φ \land (x \in X \land y \in X)) \to (M^{-1} (x) E M^{-1} (y) \leftrightarrow {({N ↾}_{dom M})}^{-1} (x) E {({N ↾}_{dom M})}^{-1} (y))$
101	16 78	syl	$⊢ φ \to M^{-1} {Isom}_{R, E} (X, dom M)$
102		isorel	$⊢ (M^{-1} {Isom}_{R, E} (X, dom M) \land (x \in X \land y \in X)) \to (x R y \leftrightarrow M^{-1} (x) E M^{-1} (y))$
103	101 102	sylan	$⊢ (φ \land (x \in X \land y \in X)) \to (x R y \leftrightarrow M^{-1} (x) E M^{-1} (y))$
104		eqidd	$⊢ φ \to N [dom M] = N [dom M]$
105		isores3	$⊢ (N {Isom}_{E, S} (dom N, Y) \land dom M \subseteq dom N \land N [dom M] = N [dom M]) \to ({N ↾}_{dom M}) {Isom}_{E, S} (dom M, N [dom M])$
106	33 8 104 105	syl3anc	$⊢ φ \to ({N ↾}_{dom M}) {Isom}_{E, S} (dom M, N [dom M])$
107		isocnv	$⊢ ({N ↾}_{dom M}) {Isom}_{E, S} (dom M, N [dom M]) \to {({N ↾}_{dom M})}^{-1} {Isom}_{S, E} (N [dom M], dom M)$
108	106 107	syl	$⊢ φ \to {({N ↾}_{dom M})}^{-1} {Isom}_{S, E} (N [dom M], dom M)$
109	108	adantr	$⊢ (φ \land (x \in X \land y \in X)) \to {({N ↾}_{dom M})}^{-1} {Isom}_{S, E} (N [dom M], dom M)$
110		simprl	$⊢ (φ \land (x \in X \land y \in X)) \to x \in X$
111	25	adantr	$⊢ (φ \land (x \in X \land y \in X)) \to X = N [dom M]$
112	110 111	eleqtrd	$⊢ (φ \land (x \in X \land y \in X)) \to x \in N [dom M]$
113		simprr	$⊢ (φ \land (x \in X \land y \in X)) \to y \in X$
114	113 111	eleqtrd	$⊢ (φ \land (x \in X \land y \in X)) \to y \in N [dom M]$
115		isorel	$⊢ ({({N ↾}_{dom M})}^{-1} {Isom}_{S, E} (N [dom M], dom M) \land (x \in N [dom M] \land y \in N [dom M])) \to (x S y \leftrightarrow {({N ↾}_{dom M})}^{-1} (x) E {({N ↾}_{dom M})}^{-1} (y))$
116	109 112 114 115	syl12anc	$⊢ (φ \land (x \in X \land y \in X)) \to (x S y \leftrightarrow {({N ↾}_{dom M})}^{-1} (x) E {({N ↾}_{dom M})}^{-1} (y))$
117	100 103 116	3bitr4d	$⊢ (φ \land (x \in X \land y \in X)) \to (x R y \leftrightarrow x S y)$
118	39	sselda	$⊢ (φ \land x \in X) \to x \in Y$
119	118	adantrr	$⊢ (φ \land (x \in X \land y \in X)) \to x \in Y$
120	119 113	jca	$⊢ (φ \land (x \in X \land y \in X)) \to (x \in Y \land y \in X)$
121	120	biantrurd	$⊢ (φ \land (x \in X \land y \in X)) \to (x S y \leftrightarrow ((x \in Y \land y \in X) \land x S y))$
122	121 49	bitr4di	$⊢ (φ \land (x \in X \land y \in X)) \to (x S y \leftrightarrow x (S \cap (Y \times X)) y)$
123	117 122	bitrd	$⊢ (φ \land (x \in X \land y \in X)) \to (x R y \leftrightarrow x (S \cap (Y \times X)) y)$
124	123	ex	$⊢ φ \to ((x \in X \land y \in X) \to (x R y \leftrightarrow x (S \cap (Y \times X)) y))$
125	48 95 124	pm5.21ndd	$⊢ φ \to (x R y \leftrightarrow x (S \cap (Y \times X)) y)$
126		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
127		df-br	$⊢ x (S \cap (Y \times X)) y \leftrightarrow ⟨x, y⟩ \in (S \cap (Y \times X))$
128	125 126 127	3bitr3g	$⊢ φ \to (⟨x, y⟩ \in R \leftrightarrow ⟨x, y⟩ \in (S \cap (Y \times X)))$
129	128	eqrelrdv2	$⊢ ((Rel R \land Rel (S \cap (Y \times X))) \land φ) \to R = S \cap (Y \times X)$
130	45 129	mpancom	$⊢ φ \to R = S \cap (Y \times X)$
131	39 130	jca	$⊢ φ \to (X \subseteq Y \land R = S \cap (Y \times X))$

Metamath Proof Explorer

Theorem fpwwe2lem8

Proof