Theorem fpwwe2lem7 9458

Description: Lemma for fpwwe2 9465. (Contributed by Mario Carneiro, 18-May-2015.)

Hypotheses

Ref	Expression
fpwwe2.1	⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2	⊢ (𝜑 → 𝐴 ∈ V)
fpwwe2.3	⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2lem9.x	⊢ (𝜑 → 𝑋𝑊𝑅)
fpwwe2lem9.y	⊢ (𝜑 → 𝑌𝑊𝑆)
fpwwe2lem9.m	⊢ 𝑀 = OrdIso(𝑅, 𝑋)
fpwwe2lem9.n	⊢ 𝑁 = OrdIso(𝑆, 𝑌)
fpwwe2lem7.1	⊢ (𝜑 → 𝐵 ∈ dom 𝑀)
fpwwe2lem7.2	⊢ (𝜑 → 𝐵 ∈ dom 𝑁)
fpwwe2lem7.3	⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))

Assertion

Ref	Expression
fpwwe2lem7	⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))))

Distinct variable groups:   𝑦,𝑢,𝐵   𝑢,𝑟,𝑥,𝑦,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦

Allowed substitution hints:   𝐴(𝑦,𝑢)   𝐵(𝑥,𝑟)   𝐶(𝑥,𝑦,𝑢,𝑟)   𝐷(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2lem7

Step	Hyp	Ref	Expression
1		fpwwe2lem9.y	. . . . . . . 8 ⊢ (𝜑 → 𝑌𝑊𝑆)
2		fpwwe2.1	. . . . . . . . . 10 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3	2	relopabi 5245	. . . . . . . . 9 ⊢ Rel 𝑊
4	3	brrelexi 5158	. . . . . . . 8 ⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V)
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ V)
6		fpwwe2.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ V)
7	2, 6	fpwwe2lem2 9454	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
8	1, 7	mpbid 222	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
9	8	simprd 479	. . . . . . . 8 ⊢ (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))
10	9	simpld 475	. . . . . . 7 ⊢ (𝜑 → 𝑆 We 𝑌)
11		fpwwe2lem9.n	. . . . . . . 8 ⊢ 𝑁 = OrdIso(𝑆, 𝑌)
12	11	oiiso 8442	. . . . . . 7 ⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
13	5, 10, 12	syl2anc 693	. . . . . 6 ⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
14	13	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
15		isof1o 6573	. . . . 5 ⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌)
16	14, 15	syl 17	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁:dom 𝑁–1-1-onto→𝑌)
17		fpwwe2.3	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
18		fpwwe2lem9.x	. . . . . 6 ⊢ (𝜑 → 𝑋𝑊𝑅)
19		fpwwe2lem9.m	. . . . . 6 ⊢ 𝑀 = OrdIso(𝑅, 𝑋)
20		fpwwe2lem7.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)
21		fpwwe2lem7.2	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ dom 𝑁)
22		fpwwe2lem7.3	. . . . . 6 ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))
23	2, 6, 17, 18, 1, 19, 11, 20, 21, 22	fpwwe2lem6 9457	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (◡𝑀‘𝐶) = (◡𝑁‘𝐶)))
24	23	simp2d 1074	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑌)
25		f1ocnvfv2 6533	. . . 4 ⊢ ((𝑁:dom 𝑁–1-1-onto→𝑌 ∧ 𝐶 ∈ 𝑌) → (𝑁‘(◡𝑁‘𝐶)) = 𝐶)
26	16, 24, 25	syl2anc 693	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁‘(◡𝑁‘𝐶)) = 𝐶)
27	23	simp3d 1075	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶))
28	3	brrelexi 5158	. . . . . . . . . . . 12 ⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V)
29	18, 28	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ V)
30	2, 6	fpwwe2lem2 9454	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
31	18, 30	mpbid 222	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
32	31	simprd 479	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
33	32	simpld 475	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 We 𝑋)
34	19	oiiso 8442	. . . . . . . . . . 11 ⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
35	29, 33, 34	syl2anc 693	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
36	35	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37		isof1o 6573	. . . . . . . . 9 ⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋)
38	36, 37	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀:dom 𝑀–1-1-onto→𝑋)
39	23	simp1d 1073	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑋)
40		f1ocnvfv2 6533	. . . . . . . 8 ⊢ ((𝑀:dom 𝑀–1-1-onto→𝑋 ∧ 𝐶 ∈ 𝑋) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶)
41	38, 39, 40	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶)) = 𝐶)
42		simpr 477	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑅(𝑀‘𝐵))
43	41, 42	eqbrtrd 4675	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵))
44		f1ocnv 6149	. . . . . . . . 9 ⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → ◡𝑀:𝑋–1-1-onto→dom 𝑀)
45		f1of 6137	. . . . . . . . 9 ⊢ (◡𝑀:𝑋–1-1-onto→dom 𝑀 → ◡𝑀:𝑋⟶dom 𝑀)
46	38, 44, 45	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑀:𝑋⟶dom 𝑀)
47	46, 39	ffvelrnd 6360	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) ∈ dom 𝑀)
48	20	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑀)
49		isorel 6576	. . . . . . 7 ⊢ ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((◡𝑀‘𝐶) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵)))
50	36, 47, 48, 49	syl12anc 1324	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(◡𝑀‘𝐶))𝑅(𝑀‘𝐵)))
51	43, 50	mpbird 247	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐶) E 𝐵)
52	27, 51	eqbrtrrd 4677	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑁‘𝐶) E 𝐵)
53		f1ocnv 6149	. . . . . . 7 ⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → ◡𝑁:𝑌–1-1-onto→dom 𝑁)
54		f1of 6137	. . . . . . 7 ⊢ (◡𝑁:𝑌–1-1-onto→dom 𝑁 → ◡𝑁:𝑌⟶dom 𝑁)
55	16, 53, 54	3syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ◡𝑁:𝑌⟶dom 𝑁)
56	55, 24	ffvelrnd 6360	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (◡𝑁‘𝐶) ∈ dom 𝑁)
57	21	adantr 481	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑁)
58		isorel 6576	. . . . 5 ⊢ ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ ((◡𝑁‘𝐶) ∈ dom 𝑁 ∧ 𝐵 ∈ dom 𝑁)) → ((◡𝑁‘𝐶) E 𝐵 ↔ (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵)))
59	14, 56, 57, 58	syl12anc 1324	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((◡𝑁‘𝐶) E 𝐵 ↔ (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵)))
60	52, 59	mpbid 222	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁‘(◡𝑁‘𝐶))𝑆(𝑁‘𝐵))
61	26, 60	eqbrtrrd 4677	. 2 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑆(𝑁‘𝐵))
62	27	adantrr 753	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (◡𝑀‘𝐶) = (◡𝑁‘𝐶))
63	2, 6, 17, 18, 1, 19, 11, 20, 21, 22	fpwwe2lem6 9457	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → (𝐷 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌 ∧ (◡𝑀‘𝐷) = (◡𝑁‘𝐷)))
64	63	simp3d 1075	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → (◡𝑀‘𝐷) = (◡𝑁‘𝐷))
65	64	adantrl 752	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (◡𝑀‘𝐷) = (◡𝑁‘𝐷))
66	62, 65	breq12d 4666	. . . 4 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ((◡𝑀‘𝐶) E (◡𝑀‘𝐷) ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷)))
67	35	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
68		isocnv 6580	. . . . . 6 ⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
69	67, 68	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
70	39	adantrr 753	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐶 ∈ 𝑋)
71	31	simpld 475	. . . . . . . . . 10 ⊢ (𝜑 → (𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)))
72	71	simprd 479	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋))
73	72	ssbrd 4696	. . . . . . . 8 ⊢ (𝜑 → (𝐷𝑅(𝑀‘𝐵) → 𝐷(𝑋 × 𝑋)(𝑀‘𝐵)))
74	73	imp 445	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷(𝑋 × 𝑋)(𝑀‘𝐵))
75		brxp 5147	. . . . . . . 8 ⊢ (𝐷(𝑋 × 𝑋)(𝑀‘𝐵) ↔ (𝐷 ∈ 𝑋 ∧ (𝑀‘𝐵) ∈ 𝑋))
76	75	simplbi 476	. . . . . . 7 ⊢ (𝐷(𝑋 × 𝑋)(𝑀‘𝐵) → 𝐷 ∈ 𝑋)
77	74, 76	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷 ∈ 𝑋)
78	77	adantrl 752	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐷 ∈ 𝑋)
79		isorel 6576	. . . . 5 ⊢ ((◡𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐶𝑅𝐷 ↔ (◡𝑀‘𝐶) E (◡𝑀‘𝐷)))
80	69, 70, 78, 79	syl12anc 1324	. . . 4 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑅𝐷 ↔ (◡𝑀‘𝐶) E (◡𝑀‘𝐷)))
81	13	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
82		isocnv 6580	. . . . . 6 ⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
83	81, 82	syl 17	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → ◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
84	24	adantrr 753	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐶 ∈ 𝑌)
85	63	simp2d 1074	. . . . . 6 ⊢ ((𝜑 ∧ 𝐷𝑅(𝑀‘𝐵)) → 𝐷 ∈ 𝑌)
86	85	adantrl 752	. . . . 5 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → 𝐷 ∈ 𝑌)
87		isorel 6576	. . . . 5 ⊢ ((◡𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝐶 ∈ 𝑌 ∧ 𝐷 ∈ 𝑌)) → (𝐶𝑆𝐷 ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷)))
88	83, 84, 86, 87	syl12anc 1324	. . . 4 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑆𝐷 ↔ (◡𝑁‘𝐶) E (◡𝑁‘𝐷)))
89	66, 80, 88	3bitr4d 300	. . 3 ⊢ ((𝜑 ∧ (𝐶𝑅(𝑀‘𝐵) ∧ 𝐷𝑅(𝑀‘𝐵))) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))
90	89	expr 643	. 2 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷)))
91	61, 90	jca 554	1 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶𝑆(𝑁‘𝐵) ∧ (𝐷𝑅(𝑀‘𝐵) → (𝐶𝑅𝐷 ↔ 𝐶𝑆𝐷))))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  Vcvv 3200  [wsbc 3435   ∩ cin 3573   ⊆ wss 3574  {csn 4177   class class class wbr 4653  {copab 4712   E cep 5028   We wwe 5072   × cxp 5112  ^◡ccnv 5113  dom cdm 5114   ↾ cres 5116   “ cima 5117  ⟶wf 5884  –1-1-onto→wf1o 5887  ‘cfv 5888   Isom wiso 5889  (class class class)co 6650  OrdIsocoi 8414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-wrecs 7407  df-recs 7468  df-oi 8415

This theorem is referenced by:  fpwwe2lem8  9459