fpwwe2lem7

Description: Lemma for fpwwe2 . Show by induction that the two isometries M and N agree on their common domain. (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	fpwwe2lem7	$⊢ φ \to M = {N ↾}_{dom M}$

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	6	oif	$⊢ M : dom M ⟶ X$
10		ffn	$⊢ M : dom M ⟶ X \to M Fn dom M$
11	9 10	mp1i	$⊢ φ \to M Fn dom M$
12	7	oif	$⊢ N : dom N ⟶ Y$
13		ffn	$⊢ N : dom N ⟶ Y \to N Fn dom N$
14	12 13	mp1i	$⊢ φ \to N Fn dom N$
15	14 8	fnssresd	$⊢ φ \to ({N ↾}_{dom M}) Fn dom M$
16	6	oicl	$⊢ Ord dom M$
17		ordelon	$⊢ (Ord dom M \land w \in dom M) \to w \in On$
18	16 17	mpan	$⊢ w \in dom M \to w \in On$
19		eleq1w	$⊢ w = y \to (w \in dom M \leftrightarrow y \in dom M)$
20		fveq2	$⊢ w = y \to M (w) = M (y)$
21		fveq2	$⊢ w = y \to N (w) = N (y)$
22	20 21	eqeq12d	$⊢ w = y \to (M (w) = N (w) \leftrightarrow M (y) = N (y))$
23	19 22	imbi12d	$⊢ w = y \to ((w \in dom M \to M (w) = N (w)) \leftrightarrow (y \in dom M \to M (y) = N (y)))$
24	23	imbi2d	$⊢ w = y \to ((φ \to (w \in dom M \to M (w) = N (w))) \leftrightarrow (φ \to (y \in dom M \to M (y) = N (y))))$
25		r19.21v	$⊢ \forall y \in w (φ \to (y \in dom M \to M (y) = N (y))) \leftrightarrow (φ \to \forall y \in w (y \in dom M \to M (y) = N (y)))$
26	16	a1i	$⊢ φ \to Ord dom M$
27		ordelss	$⊢ (Ord dom M \land w \in dom M) \to w \subseteq dom M$
28	26 27	sylan	$⊢ (φ \land w \in dom M) \to w \subseteq dom M$
29	28	sselda	$⊢ ((φ \land w \in dom M) \land y \in w) \to y \in dom M$
30		pm2.27	$⊢ y \in dom M \to ((y \in dom M \to M (y) = N (y)) \to M (y) = N (y))$
31	29 30	syl	$⊢ ((φ \land w \in dom M) \land y \in w) \to ((y \in dom M \to M (y) = N (y)) \to M (y) = N (y))$
32	31	ralimdva	$⊢ (φ \land w \in dom M) \to (\forall y \in w (y \in dom M \to M (y) = N (y)) \to \forall y \in w M (y) = N (y))$
33		fnssres	$⊢ (M Fn dom M \land w \subseteq dom M) \to ({M ↾}_{w}) Fn w$
34	11 28 33	syl2an2r	$⊢ (φ \land w \in dom M) \to ({M ↾}_{w}) Fn w$
35	8	adantr	$⊢ (φ \land w \in dom M) \to dom M \subseteq dom N$
36	28 35	sstrd	$⊢ (φ \land w \in dom M) \to w \subseteq dom N$
37		fnssres	$⊢ (N Fn dom N \land w \subseteq dom N) \to ({N ↾}_{w}) Fn w$
38	14 36 37	syl2an2r	$⊢ (φ \land w \in dom M) \to ({N ↾}_{w}) Fn w$
39		eqfnfv	$⊢ (({M ↾}_{w}) Fn w \land ({N ↾}_{w}) Fn w) \to ({M ↾}_{w} = {N ↾}_{w} \leftrightarrow \forall y \in w ({M ↾}_{w}) (y) = ({N ↾}_{w}) (y))$
40	34 38 39	syl2anc	$⊢ (φ \land w \in dom M) \to ({M ↾}_{w} = {N ↾}_{w} \leftrightarrow \forall y \in w ({M ↾}_{w}) (y) = ({N ↾}_{w}) (y))$
41		fvres	$⊢ y \in w \to ({M ↾}_{w}) (y) = M (y)$
42		fvres	$⊢ y \in w \to ({N ↾}_{w}) (y) = N (y)$
43	41 42	eqeq12d	$⊢ y \in w \to (({M ↾}_{w}) (y) = ({N ↾}_{w}) (y) \leftrightarrow M (y) = N (y))$
44	43	ralbiia	$⊢ \forall y \in w ({M ↾}_{w}) (y) = ({N ↾}_{w}) (y) \leftrightarrow \forall y \in w M (y) = N (y)$
45	40 44	bitrdi	$⊢ (φ \land w \in dom M) \to ({M ↾}_{w} = {N ↾}_{w} \leftrightarrow \forall y \in w M (y) = N (y))$
46	2	ad2antrr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to A \in V$
47		simpll	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to φ$
48	47 3	sylan	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
49	4	ad2antrr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to X W R$
50	5	ad2antrr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to Y W S$
51		simplr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to w \in dom M$
52	8	sselda	$⊢ (φ \land w \in dom M) \to w \in dom N$
53	52	adantr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to w \in dom N$
54		simpr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to {M ↾}_{w} = {N ↾}_{w}$
55	1 46 48 49 50 6 7 51 53 54	fpwwe2lem6	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land y R M (w)) \to (y S N (w) \land (z R M (w) \to (y R z \leftrightarrow y S z)))$
56	55	simpld	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land y R M (w)) \to y S N (w)$
57	54	eqcomd	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to {N ↾}_{w} = {M ↾}_{w}$
58	1 46 48 50 49 7 6 53 51 57	fpwwe2lem6	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land y S N (w)) \to (y R M (w) \land (z S N (w) \to (y S z \leftrightarrow y R z)))$
59	58	simpld	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land y S N (w)) \to y R M (w)$
60	56 59	impbida	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to (y R M (w) \leftrightarrow y S N (w))$
61		fvex	$⊢ M (w) \in V$
62		vex	$⊢ y \in V$
63	62	eliniseg	$⊢ M (w) \in V \to (y \in R^{-1} [\{M (w)\}] \leftrightarrow y R M (w))$
64	61 63	ax-mp	$⊢ y \in R^{-1} [\{M (w)\}] \leftrightarrow y R M (w)$
65		fvex	$⊢ N (w) \in V$
66	62	eliniseg	$⊢ N (w) \in V \to (y \in S^{-1} [\{N (w)\}] \leftrightarrow y S N (w))$
67	65 66	ax-mp	$⊢ y \in S^{-1} [\{N (w)\}] \leftrightarrow y S N (w)$
68	60 64 67	3bitr4g	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to (y \in R^{-1} [\{M (w)\}] \leftrightarrow y \in S^{-1} [\{N (w)\}])$
69	68	eqrdv	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R^{-1} [\{M (w)\}] = S^{-1} [\{N (w)\}]$
70		relinxp	$⊢ Rel (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]))$
71		relinxp	$⊢ Rel (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]))$
72		vex	$⊢ z \in V$
73	72	eliniseg	$⊢ M (w) \in V \to (z \in R^{-1} [\{M (w)\}] \leftrightarrow z R M (w))$
74	63 73	anbi12d	$⊢ M (w) \in V \to ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \leftrightarrow (y R M (w) \land z R M (w)))$
75	61 74	ax-mp	$⊢ (y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \leftrightarrow (y R M (w) \land z R M (w))$
76	55	simprd	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land y R M (w)) \to (z R M (w) \to (y R z \leftrightarrow y S z))$
77	76	impr	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land (y R M (w) \land z R M (w))) \to (y R z \leftrightarrow y S z)$
78	75 77	sylan2b	$⊢ (((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \land (y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}])) \to (y R z \leftrightarrow y S z)$
79	78	pm5.32da	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to (((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y R z) \leftrightarrow ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y S z))$
80		df-br	$⊢ y (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) z \leftrightarrow ⟨y, z⟩ \in (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]))$
81		brinxp2	$⊢ y (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) z \leftrightarrow ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y R z)$
82	80 81	bitr3i	$⊢ ⟨y, z⟩ \in (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) \leftrightarrow ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y R z)$
83		df-br	$⊢ y (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) z \leftrightarrow ⟨y, z⟩ \in (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]))$
84		brinxp2	$⊢ y (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) z \leftrightarrow ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y S z)$
85	83 84	bitr3i	$⊢ ⟨y, z⟩ \in (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) \leftrightarrow ((y \in R^{-1} [\{M (w)\}] \land z \in R^{-1} [\{M (w)\}]) \land y S z)$
86	79 82 85	3bitr4g	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to (⟨y, z⟩ \in (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) \leftrightarrow ⟨y, z⟩ \in (S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])))$
87	70 71 86	eqrelrdv	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]) = S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])$
88	69	sqxpeqd	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}] = S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}]$
89	88	ineq2d	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to S \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]) = S \cap (S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}])$
90	87 89	eqtrd	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}]) = S \cap (S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}])$
91	69 90	oveq12d	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R^{-1} [\{M (w)\}] F (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) = S^{-1} [\{N (w)\}] F (S \cap (S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}]))$
92	9	ffvelcdmi	$⊢ w \in dom M \to M (w) \in X$
93	92	adantl	$⊢ (φ \land w \in dom M) \to M (w) \in X$
94	93	adantr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to M (w) \in X$
95	1 2 4	fpwwe2lem3	$⊢ (φ \land M (w) \in X) \to R^{-1} [\{M (w)\}] F (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) = M (w)$
96	47 94 95	syl2anc	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to R^{-1} [\{M (w)\}] F (R \cap (R^{-1} [\{M (w)\}] \times R^{-1} [\{M (w)\}])) = M (w)$
97	12	ffvelcdmi	$⊢ w \in dom N \to N (w) \in Y$
98	52 97	syl	$⊢ (φ \land w \in dom M) \to N (w) \in Y$
99	98	adantr	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to N (w) \in Y$
100	1 2 5	fpwwe2lem3	$⊢ (φ \land N (w) \in Y) \to S^{-1} [\{N (w)\}] F (S \cap (S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}])) = N (w)$
101	47 99 100	syl2anc	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to S^{-1} [\{N (w)\}] F (S \cap (S^{-1} [\{N (w)\}] \times S^{-1} [\{N (w)\}])) = N (w)$
102	91 96 101	3eqtr3d	$⊢ ((φ \land w \in dom M) \land {M ↾}_{w} = {N ↾}_{w}) \to M (w) = N (w)$
103	102	ex	$⊢ (φ \land w \in dom M) \to ({M ↾}_{w} = {N ↾}_{w} \to M (w) = N (w))$
104	45 103	sylbird	$⊢ (φ \land w \in dom M) \to (\forall y \in w M (y) = N (y) \to M (w) = N (w))$
105	32 104	syld	$⊢ (φ \land w \in dom M) \to (\forall y \in w (y \in dom M \to M (y) = N (y)) \to M (w) = N (w))$
106	105	ex	$⊢ φ \to (w \in dom M \to (\forall y \in w (y \in dom M \to M (y) = N (y)) \to M (w) = N (w)))$
107	106	com23	$⊢ φ \to (\forall y \in w (y \in dom M \to M (y) = N (y)) \to (w \in dom M \to M (w) = N (w)))$
108	107	a2i	$⊢ (φ \to \forall y \in w (y \in dom M \to M (y) = N (y))) \to (φ \to (w \in dom M \to M (w) = N (w)))$
109	25 108	sylbi	$⊢ \forall y \in w (φ \to (y \in dom M \to M (y) = N (y))) \to (φ \to (w \in dom M \to M (w) = N (w)))$
110	109	a1i	$⊢ w \in On \to (\forall y \in w (φ \to (y \in dom M \to M (y) = N (y))) \to (φ \to (w \in dom M \to M (w) = N (w))))$
111	24 110	tfis2	$⊢ w \in On \to (φ \to (w \in dom M \to M (w) = N (w)))$
112	111	com3l	$⊢ φ \to (w \in dom M \to (w \in On \to M (w) = N (w)))$
113	18 112	mpdi	$⊢ φ \to (w \in dom M \to M (w) = N (w))$
114	113	imp	$⊢ (φ \land w \in dom M) \to M (w) = N (w)$
115		fvres	$⊢ w \in dom M \to ({N ↾}_{dom M}) (w) = N (w)$
116	115	adantl	$⊢ (φ \land w \in dom M) \to ({N ↾}_{dom M}) (w) = N (w)$
117	114 116	eqtr4d	$⊢ (φ \land w \in dom M) \to M (w) = ({N ↾}_{dom M}) (w)$
118	11 15 117	eqfnfvd	$⊢ φ \to M = {N ↾}_{dom M}$

Metamath Proof Explorer

Theorem fpwwe2lem7

Proof