fpwwe2lem6

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	fpwwe2lem6	$⊢ (φ \land C R M (B)) \to (C S N (B) \land (D R M (B) \to (C R D \leftrightarrow C S D)))$

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	relopabiv	$⊢ Rel W$
12	11	brrelex1i	$⊢ Y W S \to Y \in V$
13	5 12	syl	$⊢ φ \to Y \in V$
14	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)))$
15	5 14	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))$
16	15	simprld	$⊢ φ \to S We Y$
17	7	oiiso	$⊢ (Y \in V \land S We Y) \to N {Isom}_{E, S} (dom N, Y)$
18	13 16 17	syl2anc	$⊢ φ \to N {Isom}_{E, S} (dom N, Y)$
19	18	adantr	$⊢ (φ \land C R M (B)) \to N {Isom}_{E, S} (dom N, Y)$
20		isof1o	$⊢ N {Isom}_{E, S} (dom N, Y) \to N : dom N \underset{1-1 onto}{⟶} Y$
21	19 20	syl	$⊢ (φ \land C R M (B)) \to N : dom N \underset{1-1 onto}{⟶} Y$
22	1 2 3 4 5 6 7 8 9 10	fpwwe2lem5	$⊢ (φ \land C R M (B)) \to (C \in X \land C \in Y \land M^{-1} (C) = N^{-1} (C))$
23	22	simp2d	$⊢ (φ \land C R M (B)) \to C \in Y$
24		f1ocnvfv2	$⊢ (N : dom N \underset{1-1 onto}{⟶} Y \land C \in Y) \to N (N^{-1} (C)) = C$
25	21 23 24	syl2anc	$⊢ (φ \land C R M (B)) \to N (N^{-1} (C)) = C$
26	22	simp3d	$⊢ (φ \land C R M (B)) \to M^{-1} (C) = N^{-1} (C)$
27	11	brrelex1i	$⊢ X W R \to X \in V$
28	4 27	syl	$⊢ φ \to X \in V$
29	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)))$
30	4 29	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))$
31	30	simprld	$⊢ φ \to R We X$
32	6	oiiso	$⊢ (X \in V \land R We X) \to M {Isom}_{E, R} (dom M, X)$
33	28 31 32	syl2anc	$⊢ φ \to M {Isom}_{E, R} (dom M, X)$
34	33	adantr	$⊢ (φ \land C R M (B)) \to M {Isom}_{E, R} (dom M, X)$
35		isof1o	$⊢ M {Isom}_{E, R} (dom M, X) \to M : dom M \underset{1-1 onto}{⟶} X$
36	34 35	syl	$⊢ (φ \land C R M (B)) \to M : dom M \underset{1-1 onto}{⟶} X$
37	22	simp1d	$⊢ (φ \land C R M (B)) \to C \in X$
38		f1ocnvfv2	$⊢ (M : dom M \underset{1-1 onto}{⟶} X \land C \in X) \to M (M^{-1} (C)) = C$
39	36 37 38	syl2anc	$⊢ (φ \land C R M (B)) \to M (M^{-1} (C)) = C$
40		simpr	$⊢ (φ \land C R M (B)) \to C R M (B)$
41	39 40	eqbrtrd	$⊢ (φ \land C R M (B)) \to M (M^{-1} (C)) R M (B)$
42		f1ocnv	$⊢ M : dom M \underset{1-1 onto}{⟶} X \to M^{-1} : X \underset{1-1 onto}{⟶} dom M$
43		f1of	$⊢ M^{-1} : X \underset{1-1 onto}{⟶} dom M \to M^{-1} : X ⟶ dom M$
44	36 42 43	3syl	$⊢ (φ \land C R M (B)) \to M^{-1} : X ⟶ dom M$
45	44 37	ffvelcdmd	$⊢ (φ \land C R M (B)) \to M^{-1} (C) \in dom M$
46	8	adantr	$⊢ (φ \land C R M (B)) \to B \in dom M$
47		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))$
48	34 45 46 47	syl12anc	$⊢ (φ \land C R M (B)) \to (M^{-1} (C) E B \leftrightarrow M (M^{-1} (C)) R M (B))$
49	41 48	mpbird	$⊢ (φ \land C R M (B)) \to M^{-1} (C) E B$
50	26 49	eqbrtrrd	$⊢ (φ \land C R M (B)) \to N^{-1} (C) E B$
51		f1ocnv	$⊢ N : dom N \underset{1-1 onto}{⟶} Y \to N^{-1} : Y \underset{1-1 onto}{⟶} dom N$
52		f1of	$⊢ N^{-1} : Y \underset{1-1 onto}{⟶} dom N \to N^{-1} : Y ⟶ dom N$
53	21 51 52	3syl	$⊢ (φ \land C R M (B)) \to N^{-1} : Y ⟶ dom N$
54	53 23	ffvelcdmd	$⊢ (φ \land C R M (B)) \to N^{-1} (C) \in dom N$
55	9	adantr	$⊢ (φ \land C R M (B)) \to B \in dom N$
56		isorel	$⊢ (N {Isom}_{E, S} (dom N, Y) \land (N^{-1} (C) \in dom N \land B \in dom N)) \to (N^{-1} (C) E B \leftrightarrow N (N^{-1} (C)) S N (B))$
57	19 54 55 56	syl12anc	$⊢ (φ \land C R M (B)) \to (N^{-1} (C) E B \leftrightarrow N (N^{-1} (C)) S N (B))$
58	50 57	mpbid	$⊢ (φ \land C R M (B)) \to N (N^{-1} (C)) S N (B)$
59	25 58	eqbrtrrd	$⊢ (φ \land C R M (B)) \to C S N (B)$
60	26	adantrr	$⊢ (φ \land (C R M (B) \land D R M (B))) \to M^{-1} (C) = N^{-1} (C)$
61	1 2 3 4 5 6 7 8 9 10	fpwwe2lem5	$⊢ (φ \land D R M (B)) \to (D \in X \land D \in Y \land M^{-1} (D) = N^{-1} (D))$
62	61	simp3d	$⊢ (φ \land D R M (B)) \to M^{-1} (D) = N^{-1} (D)$
63	62	adantrl	$⊢ (φ \land (C R M (B) \land D R M (B))) \to M^{-1} (D) = N^{-1} (D)$
64	60 63	breq12d	$⊢ (φ \land (C R M (B) \land D R M (B))) \to (M^{-1} (C) E M^{-1} (D) \leftrightarrow N^{-1} (C) E N^{-1} (D))$
65	33	adantr	$⊢ (φ \land (C R M (B) \land D R M (B))) \to M {Isom}_{E, R} (dom M, X)$
66		isocnv	$⊢ M {Isom}_{E, R} (dom M, X) \to M^{-1} {Isom}_{R, E} (X, dom M)$
67	65 66	syl	$⊢ (φ \land (C R M (B) \land D R M (B))) \to M^{-1} {Isom}_{R, E} (X, dom M)$
68	37	adantrr	$⊢ (φ \land (C R M (B) \land D R M (B))) \to C \in X$
69	30	simplrd	$⊢ φ \to R \subseteq X \times X$
70	69	ssbrd	$⊢ φ \to (D R M (B) \to D (X \times X) M (B))$
71	70	imp	$⊢ (φ \land D R M (B)) \to D (X \times X) M (B)$
72		brxp	$⊢ D (X \times X) M (B) \leftrightarrow (D \in X \land M (B) \in X)$
73	72	simplbi	$⊢ D (X \times X) M (B) \to D \in X$
74	71 73	syl	$⊢ (φ \land D R M (B)) \to D \in X$
75	74	adantrl	$⊢ (φ \land (C R M (B) \land D R M (B))) \to D \in X$
76		isorel	$⊢ (M^{-1} {Isom}_{R, E} (X, dom M) \land (C \in X \land D \in X)) \to (C R D \leftrightarrow M^{-1} (C) E M^{-1} (D))$
77	67 68 75 76	syl12anc	$⊢ (φ \land (C R M (B) \land D R M (B))) \to (C R D \leftrightarrow M^{-1} (C) E M^{-1} (D))$
78	18	adantr	$⊢ (φ \land (C R M (B) \land D R M (B))) \to N {Isom}_{E, S} (dom N, Y)$
79		isocnv	$⊢ N {Isom}_{E, S} (dom N, Y) \to N^{-1} {Isom}_{S, E} (Y, dom N)$
80	78 79	syl	$⊢ (φ \land (C R M (B) \land D R M (B))) \to N^{-1} {Isom}_{S, E} (Y, dom N)$
81	23	adantrr	$⊢ (φ \land (C R M (B) \land D R M (B))) \to C \in Y$
82	61	simp2d	$⊢ (φ \land D R M (B)) \to D \in Y$
83	82	adantrl	$⊢ (φ \land (C R M (B) \land D R M (B))) \to D \in Y$
84		isorel	$⊢ (N^{-1} {Isom}_{S, E} (Y, dom N) \land (C \in Y \land D \in Y)) \to (C S D \leftrightarrow N^{-1} (C) E N^{-1} (D))$
85	80 81 83 84	syl12anc	$⊢ (φ \land (C R M (B) \land D R M (B))) \to (C S D \leftrightarrow N^{-1} (C) E N^{-1} (D))$
86	64 77 85	3bitr4d	$⊢ (φ \land (C R M (B) \land D R M (B))) \to (C R D \leftrightarrow C S D)$
87	86	expr	$⊢ (φ \land C R M (B)) \to (D R M (B) \to (C R D \leftrightarrow C S D))$
88	59 87	jca	$⊢ (φ \land C R M (B)) \to (C S N (B) \land (D R M (B) \to (C R D \leftrightarrow C S D)))$

Metamath Proof Explorer

Theorem fpwwe2lem6

Proof