fpwwe2lem5 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fpwwe2lem5		Structured version Visualization version GIF version

Theorem fpwwe2lem5 10658

Description: Lemma for fpwwe2 10666. (Contributed by Mario Carneiro, 18-May-2015.) (Revised by AV, 20-Jul-2024.)

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

**Assertion**
Ref	Expression
fpwwe2lem5	⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (^◡𝑀‘𝐶) = (^◡𝑁‘𝐶)))

Distinct variable groups: 𝑦,𝑢,𝐵 𝑢,𝑟,𝑥,𝑦,𝐹 𝑋,𝑟,𝑢,𝑥,𝑦 𝑀,𝑟,𝑢,𝑥,𝑦 𝑁,𝑟,𝑢,𝑥,𝑦 𝜑,𝑟,𝑢,𝑥,𝑦 𝐴,𝑟,𝑥 𝑅,𝑟,𝑢,𝑥,𝑦 𝑌,𝑟,𝑢,𝑥,𝑦 𝑆,𝑟,𝑢,𝑥,𝑦 𝑊,𝑟,𝑢,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑦,𝑢) 𝐵(𝑥,𝑟) 𝐶(𝑥,𝑦,𝑢,𝑟) 𝑉(𝑥,𝑦,𝑢,𝑟)

**Proof of Theorem fpwwe2lem5**
Step	Hyp	Ref	Expression
1		fpwwe2lem8.x	. . . . . . 7 ⊢ (𝜑 → 𝑋𝑊𝑅)
2		fpwwe2.1	. . . . . . . 8 ⊢ 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 [(^◡𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3		fpwwe2.2	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
4	2, 3	fpwwe2lem2 10655	. . . . . . 7 ⊢ (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
5	1, 4	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦 ∈ 𝑋 [(^◡𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
6	5	simplrd 768	. . . . 5 ⊢ (𝜑 → 𝑅 ⊆ (𝑋 × 𝑋))
7	6	ssbrd 5186	. . . 4 ⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶(𝑋 × 𝑋)(𝑀‘𝐵)))
8		brxp 5721	. . . . 5 ⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (𝑀‘𝐵) ∈ 𝑋))
9	8	simplbi 496	. . . 4 ⊢ (𝐶(𝑋 × 𝑋)(𝑀‘𝐵) → 𝐶 ∈ 𝑋)
10	7, 9	syl6 35	. . 3 ⊢ (𝜑 → (𝐶𝑅(𝑀‘𝐵) → 𝐶 ∈ 𝑋))
11	10	imp 405	. 2 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑋)
12		imassrn 6069	. . . 4 ⊢ (𝑁 “ 𝐵) ⊆ ran 𝑁
13		fpwwe2lem8.y	. . . . . . . . 9 ⊢ (𝜑 → 𝑌𝑊𝑆)
14	2	relopabiv 5816	. . . . . . . . . 10 ⊢ Rel 𝑊
15	14	brrelex1i 5728	. . . . . . . . 9 ⊢ (𝑌𝑊𝑆 → 𝑌 ∈ V)
16	13, 15	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ V)
17	2, 3	fpwwe2lem2 10655	. . . . . . . . . 10 ⊢ (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(^◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
18	13, 17	mpbid 231	. . . . . . . . 9 ⊢ (𝜑 → ((𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦 ∈ 𝑌 [(^◡𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
19	18	simprld 770	. . . . . . . 8 ⊢ (𝜑 → 𝑆 We 𝑌)
20		fpwwe2lem8.n	. . . . . . . . 9 ⊢ 𝑁 = OrdIso(𝑆, 𝑌)
21	20	oiiso 9560	. . . . . . . 8 ⊢ ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
22	16, 19, 21	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
23	22	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
24		isof1o 7327	. . . . . 6 ⊢ (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁–1-1-onto→𝑌)
25	23, 24	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑁:dom 𝑁–1-1-onto→𝑌)
26		f1ofo 6841	. . . . 5 ⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → 𝑁:dom 𝑁–onto→𝑌)
27		forn 6809	. . . . 5 ⊢ (𝑁:dom 𝑁–onto→𝑌 → ran 𝑁 = 𝑌)
28	25, 26, 27	3syl 18	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran 𝑁 = 𝑌)
29	12, 28	sseqtrid 4025	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑁 “ 𝐵) ⊆ 𝑌)
30	14	brrelex1i 5728	. . . . . . . . . . . . . 14 ⊢ (𝑋𝑊𝑅 → 𝑋 ∈ V)
31	1, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑋 ∈ V)
32	5	simprld 770	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 We 𝑋)
33		fpwwe2lem8.m	. . . . . . . . . . . . . 14 ⊢ 𝑀 = OrdIso(𝑅, 𝑋)
34	33	oiiso 9560	. . . . . . . . . . . . 13 ⊢ ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
35	31, 32, 34	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
36	35	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37		isof1o 7327	. . . . . . . . . . 11 ⊢ (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀–1-1-onto→𝑋)
38	36, 37	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝑀:dom 𝑀–1-1-onto→𝑋)
39		f1ocnvfv2 7282	. . . . . . . . . 10 ⊢ ((𝑀:dom 𝑀–1-1-onto→𝑋 ∧ 𝐶 ∈ 𝑋) → (𝑀‘(^◡𝑀‘𝐶)) = 𝐶)
40	38, 11, 39	syl2anc 582	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(^◡𝑀‘𝐶)) = 𝐶)
41		simpr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶𝑅(𝑀‘𝐵))
42	40, 41	eqbrtrd 5165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀‘(^◡𝑀‘𝐶))𝑅(𝑀‘𝐵))
43		f1ocnv 6846	. . . . . . . . . . 11 ⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → ^◡𝑀:𝑋–1-1-onto→dom 𝑀)
44		f1of 6834	. . . . . . . . . . 11 ⊢ (^◡𝑀:𝑋–1-1-onto→dom 𝑀 → ^◡𝑀:𝑋⟶dom 𝑀)
45	38, 43, 44	3syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ^◡𝑀:𝑋⟶dom 𝑀)
46	45, 11	ffvelcdmd 7090	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (^◡𝑀‘𝐶) ∈ dom 𝑀)
47		fpwwe2lem5.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ dom 𝑀)
48	47	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐵 ∈ dom 𝑀)
49		isorel 7330	. . . . . . . . 9 ⊢ ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((^◡𝑀‘𝐶) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀)) → ((^◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(^◡𝑀‘𝐶))𝑅(𝑀‘𝐵)))
50	36, 46, 48, 49	syl12anc 835	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((^◡𝑀‘𝐶) E 𝐵 ↔ (𝑀‘(^◡𝑀‘𝐶))𝑅(𝑀‘𝐵)))
51	42, 50	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (^◡𝑀‘𝐶) E 𝐵)
52		epelg 5577	. . . . . . . 8 ⊢ (𝐵 ∈ dom 𝑀 → ((^◡𝑀‘𝐶) E 𝐵 ↔ (^◡𝑀‘𝐶) ∈ 𝐵))
53	48, 52	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((^◡𝑀‘𝐶) E 𝐵 ↔ (^◡𝑀‘𝐶) ∈ 𝐵))
54	51, 53	mpbid 231	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (^◡𝑀‘𝐶) ∈ 𝐵)
55		ffn 6717	. . . . . . 7 ⊢ (^◡𝑀:𝑋⟶dom 𝑀 → ^◡𝑀 Fn 𝑋)
56		elpreima 7062	. . . . . . 7 ⊢ (^◡𝑀 Fn 𝑋 → (𝐶 ∈ (^◡^◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (^◡𝑀‘𝐶) ∈ 𝐵)))
57	45, 55, 56	3syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ (^◡^◡𝑀 “ 𝐵) ↔ (𝐶 ∈ 𝑋 ∧ (^◡𝑀‘𝐶) ∈ 𝐵)))
58	11, 54, 57	mpbir2and 711	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (^◡^◡𝑀 “ 𝐵))
59		imacnvcnv 6205	. . . . 5 ⊢ (^◡^◡𝑀 “ 𝐵) = (𝑀 “ 𝐵)
60	58, 59	eleqtrdi 2835	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑀 “ 𝐵))
61		fpwwe2lem5.3	. . . . . . 7 ⊢ (𝜑 → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))
62	61	adantr 479	. . . . . 6 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 ↾ 𝐵) = (𝑁 ↾ 𝐵))
63	62	rneqd 5934	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ran (𝑀 ↾ 𝐵) = ran (𝑁 ↾ 𝐵))
64		df-ima 5685	. . . . 5 ⊢ (𝑀 “ 𝐵) = ran (𝑀 ↾ 𝐵)
65		df-ima 5685	. . . . 5 ⊢ (𝑁 “ 𝐵) = ran (𝑁 ↾ 𝐵)
66	63, 64, 65	3eqtr4g 2790	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝑀 “ 𝐵) = (𝑁 “ 𝐵))
67	60, 66	eleqtrd 2827	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ (𝑁 “ 𝐵))
68	29, 67	sseldd 3973	. 2 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → 𝐶 ∈ 𝑌)
69	62	cnveqd 5872	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ^◡(𝑀 ↾ 𝐵) = ^◡(𝑁 ↾ 𝐵))
70		dff1o3 6840	. . . . . . 7 ⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 ↔ (𝑀:dom 𝑀–onto→𝑋 ∧ Fun ^◡𝑀))
71	70	simprbi 495	. . . . . 6 ⊢ (𝑀:dom 𝑀–1-1-onto→𝑋 → Fun ^◡𝑀)
72		funcnvres 6626	. . . . . 6 ⊢ (Fun ^◡𝑀 → ^◡(𝑀 ↾ 𝐵) = (^◡𝑀 ↾ (𝑀 “ 𝐵)))
73	38, 71, 72	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ^◡(𝑀 ↾ 𝐵) = (^◡𝑀 ↾ (𝑀 “ 𝐵)))
74		dff1o3 6840	. . . . . . 7 ⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 ↔ (𝑁:dom 𝑁–onto→𝑌 ∧ Fun ^◡𝑁))
75	74	simprbi 495	. . . . . 6 ⊢ (𝑁:dom 𝑁–1-1-onto→𝑌 → Fun ^◡𝑁)
76		funcnvres 6626	. . . . . 6 ⊢ (Fun ^◡𝑁 → ^◡(𝑁 ↾ 𝐵) = (^◡𝑁 ↾ (𝑁 “ 𝐵)))
77	25, 75, 76	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ^◡(𝑁 ↾ 𝐵) = (^◡𝑁 ↾ (𝑁 “ 𝐵)))
78	69, 73, 77	3eqtr3d 2773	. . . 4 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (^◡𝑀 ↾ (𝑀 “ 𝐵)) = (^◡𝑁 ↾ (𝑁 “ 𝐵)))
79	78	fveq1d 6894	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((^◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = ((^◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶))
80	60	fvresd 6912	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((^◡𝑀 ↾ (𝑀 “ 𝐵))‘𝐶) = (^◡𝑀‘𝐶))
81	67	fvresd 6912	. . 3 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → ((^◡𝑁 ↾ (𝑁 “ 𝐵))‘𝐶) = (^◡𝑁‘𝐶))
82	79, 80, 81	3eqtr3d 2773	. 2 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (^◡𝑀‘𝐶) = (^◡𝑁‘𝐶))
83	11, 68, 82	3jca 1125	1 ⊢ ((𝜑 ∧ 𝐶𝑅(𝑀‘𝐵)) → (𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ (^◡𝑀‘𝐶) = (^◡𝑁‘𝐶)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3051 Vcvv 3463 [wsbc 3768 ∩ cin 3938 ⊆ wss 3939 {csn 4624 class class class wbr 5143 {copab 5205 E cep 5575 We wwe 5626 × cxp 5670 ^◡ccnv 5671 dom cdm 5672 ran crn 5673 ↾ cres 5674 “ cima 5675 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 –onto→wfo 6541 –1-1-onto→wf1o 6542 ‘cfv 6543 Isom wiso 6544 (class class class)co 7416 OrdIsocoi 9532

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7738

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-pss 3959 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7372 df-ov 7419 df-2nd 7992 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-oi 9533

This theorem is referenced by: fpwwe2lem6 10659

W3C validator