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

Metamath Proof Explorer

Theorem fpwwe2lem8

Proof