fpwwe2lem5

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-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$
	fpwwe2lem8.x	$⊢ φ \to X W R$
	fpwwe2lem8.y	$⊢ φ \to Y W S$
	fpwwe2lem8.m	$⊢ M = OrdIso (R, X)$
	fpwwe2lem8.n	$⊢ N = OrdIso (S, Y)$
	fpwwe2lem5.1	$⊢ φ \to B \in dom M$
	fpwwe2lem5.2	$⊢ φ \to B \in dom N$
	fpwwe2lem5.3	$⊢ φ \to {M ↾}_{B} = {N ↾}_{B}$
Assertion	fpwwe2lem5	$⊢ (φ \land C R M (B)) \to (C \in X \land C \in Y \land M^{-1} (C) = N^{-1} (C))$

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		fpwwe2lem5.1	$⊢ φ \to B \in dom M$
9		fpwwe2lem5.2	$⊢ φ \to B \in dom N$
10		fpwwe2lem5.3	$⊢ φ \to {M ↾}_{B} = {N ↾}_{B}$
11	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)))$
12	4 11	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))$
13	12	simplrd	$⊢ φ \to R \subseteq X \times X$
14	13	ssbrd	$⊢ φ \to (C R M (B) \to C (X \times X) M (B))$
15		brxp	$⊢ C (X \times X) M (B) \leftrightarrow (C \in X \land M (B) \in X)$
16	15	simplbi	$⊢ C (X \times X) M (B) \to C \in X$
17	14 16	syl6	$⊢ φ \to (C R M (B) \to C \in X)$
18	17	imp	$⊢ (φ \land C R M (B)) \to C \in X$
19		imassrn	$⊢ N [B] \subseteq ran N$
20	1	relopabiv	$⊢ Rel W$
21	20	brrelex1i	$⊢ Y W S \to Y \in V$
22	5 21	syl	$⊢ φ \to Y \in V$
23	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)))$
24	5 23	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))$
25	24	simprld	$⊢ φ \to S We Y$
26	7	oiiso	$⊢ (Y \in V \land S We Y) \to N {Isom}_{E, S} (dom N, Y)$
27	22 25 26	syl2anc	$⊢ φ \to N {Isom}_{E, S} (dom N, Y)$
28	27	adantr	$⊢ (φ \land C R M (B)) \to N {Isom}_{E, S} (dom N, Y)$
29		isof1o	$⊢ N {Isom}_{E, S} (dom N, Y) \to N : dom N \underset{1-1 onto}{⟶} Y$
30	28 29	syl	$⊢ (φ \land C R M (B)) \to N : dom N \underset{1-1 onto}{⟶} Y$
31		f1ofo	$⊢ N : dom N \underset{1-1 onto}{⟶} Y \to N : dom N \underset{onto}{⟶} Y$
32		forn	$⊢ N : dom N \underset{onto}{⟶} Y \to ran N = Y$
33	30 31 32	3syl	$⊢ (φ \land C R M (B)) \to ran N = Y$
34	19 33	sseqtrid	$⊢ (φ \land C R M (B)) \to N [B] \subseteq Y$
35	20	brrelex1i	$⊢ X W R \to X \in V$
36	4 35	syl	$⊢ φ \to X \in V$
37	12	simprld	$⊢ φ \to R We X$
38	6	oiiso	$⊢ (X \in V \land R We X) \to M {Isom}_{E, R} (dom M, X)$
39	36 37 38	syl2anc	$⊢ φ \to M {Isom}_{E, R} (dom M, X)$
40	39	adantr	$⊢ (φ \land C R M (B)) \to M {Isom}_{E, R} (dom M, X)$
41		isof1o	$⊢ M {Isom}_{E, R} (dom M, X) \to M : dom M \underset{1-1 onto}{⟶} X$
42	40 41	syl	$⊢ (φ \land C R M (B)) \to M : dom M \underset{1-1 onto}{⟶} X$
43		f1ocnvfv2	$⊢ (M : dom M \underset{1-1 onto}{⟶} X \land C \in X) \to M (M^{-1} (C)) = C$
44	42 18 43	syl2anc	$⊢ (φ \land C R M (B)) \to M (M^{-1} (C)) = C$
45		simpr	$⊢ (φ \land C R M (B)) \to C R M (B)$
46	44 45	eqbrtrd	$⊢ (φ \land C R M (B)) \to M (M^{-1} (C)) R M (B)$
47		f1ocnv	$⊢ M : dom M \underset{1-1 onto}{⟶} X \to M^{-1} : X \underset{1-1 onto}{⟶} dom M$
48		f1of	$⊢ M^{-1} : X \underset{1-1 onto}{⟶} dom M \to M^{-1} : X ⟶ dom M$
49	42 47 48	3syl	$⊢ (φ \land C R M (B)) \to M^{-1} : X ⟶ dom M$
50	49 18	ffvelcdmd	$⊢ (φ \land C R M (B)) \to M^{-1} (C) \in dom M$
51	8	adantr	$⊢ (φ \land C R M (B)) \to B \in dom M$
52		isorel	$⊢ (M {Isom}_{E, R} (dom M, X) \land (M^{-1} (C) \in dom M \land B \in dom M)) \to (M^{-1} (C) E B \leftrightarrow M (M^{-1} (C)) R M (B))$
53	40 50 51 52	syl12anc	$⊢ (φ \land C R M (B)) \to (M^{-1} (C) E B \leftrightarrow M (M^{-1} (C)) R M (B))$
54	46 53	mpbird	$⊢ (φ \land C R M (B)) \to M^{-1} (C) E B$
55		epelg	$⊢ B \in dom M \to (M^{-1} (C) E B \leftrightarrow M^{-1} (C) \in B)$
56	51 55	syl	$⊢ (φ \land C R M (B)) \to (M^{-1} (C) E B \leftrightarrow M^{-1} (C) \in B)$
57	54 56	mpbid	$⊢ (φ \land C R M (B)) \to M^{-1} (C) \in B$
58		ffn	$⊢ M^{-1} : X ⟶ dom M \to M^{-1} Fn X$
59		elpreima	$⊢ M^{-1} Fn X \to (C \in {M^{-1}}^{-1} [B] \leftrightarrow (C \in X \land M^{-1} (C) \in B))$
60	49 58 59	3syl	$⊢ (φ \land C R M (B)) \to (C \in {M^{-1}}^{-1} [B] \leftrightarrow (C \in X \land M^{-1} (C) \in B))$
61	18 57 60	mpbir2and	$⊢ (φ \land C R M (B)) \to C \in {M^{-1}}^{-1} [B]$
62		imacnvcnv	$⊢ {M^{-1}}^{-1} [B] = M [B]$
63	61 62	eleqtrdi	$⊢ (φ \land C R M (B)) \to C \in M [B]$
64	10	adantr	$⊢ (φ \land C R M (B)) \to {M ↾}_{B} = {N ↾}_{B}$
65	64	rneqd	$⊢ (φ \land C R M (B)) \to ran ({M ↾}_{B}) = ran ({N ↾}_{B})$
66		df-ima	$⊢ M [B] = ran ({M ↾}_{B})$
67		df-ima	$⊢ N [B] = ran ({N ↾}_{B})$
68	65 66 67	3eqtr4g	$⊢ (φ \land C R M (B)) \to M [B] = N [B]$
69	63 68	eleqtrd	$⊢ (φ \land C R M (B)) \to C \in N [B]$
70	34 69	sseldd	$⊢ (φ \land C R M (B)) \to C \in Y$
71	64	cnveqd	$⊢ (φ \land C R M (B)) \to {({M ↾}_{B})}^{-1} = {({N ↾}_{B})}^{-1}$
72		dff1o3	$⊢ M : dom M \underset{1-1 onto}{⟶} X \leftrightarrow (M : dom M \underset{onto}{⟶} X \land Fun M^{-1})$
73	72	simprbi	$⊢ M : dom M \underset{1-1 onto}{⟶} X \to Fun M^{-1}$
74		funcnvres	$⊢ Fun M^{-1} \to {({M ↾}_{B})}^{-1} = {M^{-1} ↾}_{M [B]}$
75	42 73 74	3syl	$⊢ (φ \land C R M (B)) \to {({M ↾}_{B})}^{-1} = {M^{-1} ↾}_{M [B]}$
76		dff1o3	$⊢ N : dom N \underset{1-1 onto}{⟶} Y \leftrightarrow (N : dom N \underset{onto}{⟶} Y \land Fun N^{-1})$
77	76	simprbi	$⊢ N : dom N \underset{1-1 onto}{⟶} Y \to Fun N^{-1}$
78		funcnvres	$⊢ Fun N^{-1} \to {({N ↾}_{B})}^{-1} = {N^{-1} ↾}_{N [B]}$
79	30 77 78	3syl	$⊢ (φ \land C R M (B)) \to {({N ↾}_{B})}^{-1} = {N^{-1} ↾}_{N [B]}$
80	71 75 79	3eqtr3d	$⊢ (φ \land C R M (B)) \to {M^{-1} ↾}_{M [B]} = {N^{-1} ↾}_{N [B]}$
81	80	fveq1d	$⊢ (φ \land C R M (B)) \to ({M^{-1} ↾}_{M [B]}) (C) = ({N^{-1} ↾}_{N [B]}) (C)$
82	63	fvresd	$⊢ (φ \land C R M (B)) \to ({M^{-1} ↾}_{M [B]}) (C) = M^{-1} (C)$
83	69	fvresd	$⊢ (φ \land C R M (B)) \to ({N^{-1} ↾}_{N [B]}) (C) = N^{-1} (C)$
84	81 82 83	3eqtr3d	$⊢ (φ \land C R M (B)) \to M^{-1} (C) = N^{-1} (C)$
85	18 70 84	3jca	$⊢ (φ \land C R M (B)) \to (C \in X \land C \in Y \land M^{-1} (C) = N^{-1} (C))$

Metamath Proof Explorer

Theorem fpwwe2lem5

Proof