Theorem fpwwe2lem5

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

	Ref	Expression
Hypotheses	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	fpwwe2lem5	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2		fpwwe2.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fpwwe2.3	⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4		fpwwe2lem8.x	⊢ ( 𝜑 → 𝑋 𝑊 𝑅 )
5		fpwwe2lem8.y	⊢ ( 𝜑 → 𝑌 𝑊 𝑆 )
6		fpwwe2lem8.m	⊢ 𝑀 = OrdIso ( 𝑅 , 𝑋 )
7		fpwwe2lem8.n	⊢ 𝑁 = OrdIso ( 𝑆 , 𝑌 )
8		fpwwe2lem5.1	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
9		fpwwe2lem5.2	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑁 )
10		fpwwe2lem5.3	⊢ ( 𝜑 → ( 𝑀 ↾ 𝐵 ) = ( 𝑁 ↾ 𝐵 ) )
11	1 2	fpwwe2lem2	⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
12	4 11	mpbid	⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
13	12	simplrd	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑋 × 𝑋 ) )
14	13	ssbrd	⊢ ( 𝜑 → ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) → 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) ) )
15		brxp	⊢ ( 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) ↔ ( 𝐶 ∈ 𝑋 ∧ ( 𝑀 ‘ 𝐵 ) ∈ 𝑋 ) )
16	15	simplbi	⊢ ( 𝐶 ( 𝑋 × 𝑋 ) ( 𝑀 ‘ 𝐵 ) → 𝐶 ∈ 𝑋 )
17	14 16	syl6	⊢ ( 𝜑 → ( 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) → 𝐶 ∈ 𝑋 ) )
18	17	imp	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ 𝑋 )
19		imassrn	⊢ ( 𝑁 “ 𝐵 ) ⊆ ran 𝑁
20	1	relopabiv	⊢ Rel 𝑊
21	20	brrelex1i	⊢ ( 𝑌 𝑊 𝑆 → 𝑌 ∈ V )
22	5 21	syl	⊢ ( 𝜑 → 𝑌 ∈ V )
23	1 2	fpwwe2lem2	⊢ ( 𝜑 → ( 𝑌 𝑊 𝑆 ↔ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
24	5 23	mpbid	⊢ ( 𝜑 → ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
25	24	simprld	⊢ ( 𝜑 → 𝑆 We 𝑌 )
26	7	oiiso	⊢ ( ( 𝑌 ∈ V ∧ 𝑆 We 𝑌 ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
27	22 25 26	syl2anc	⊢ ( 𝜑 → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
29		isof1o	⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 )
30	28 29	syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 )
31		f1ofo	⊢ ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 → 𝑁 : dom 𝑁 –onto→ 𝑌 )
32		forn	⊢ ( 𝑁 : dom 𝑁 –onto→ 𝑌 → ran 𝑁 = 𝑌 )
33	30 31 32	3syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ran 𝑁 = 𝑌 )
34	19 33	sseqtrid	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑁 “ 𝐵 ) ⊆ 𝑌 )
35	20	brrelex1i	⊢ ( 𝑋 𝑊 𝑅 → 𝑋 ∈ V )
36	4 35	syl	⊢ ( 𝜑 → 𝑋 ∈ V )
37	12	simprld	⊢ ( 𝜑 → 𝑅 We 𝑋 )
38	6	oiiso	⊢ ( ( 𝑋 ∈ V ∧ 𝑅 We 𝑋 ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
39	36 37 38	syl2anc	⊢ ( 𝜑 → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
41		isof1o	⊢ ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 )
42	40 41	syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 )
43		f1ocnvfv2	⊢ ( ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) = 𝐶 )
44	42 18 43	syl2anc	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) = 𝐶 )
45		simpr	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) )
46	44 45	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) )
47		f1ocnv	⊢ ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 → ◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 )
48		f1of	⊢ ( ◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 → ◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
49	42 47 48	3syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
50	49 18	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) ∈ dom 𝑀 )
51	8	adantr	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐵 ∈ dom 𝑀 )
52		isorel	⊢ ( ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) ∧ ( ( ◡ 𝑀 ‘ 𝐶 ) ∈ dom 𝑀 ∧ 𝐵 ∈ dom 𝑀 ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) ) )
53	40 50 51 52	syl12anc	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( 𝑀 ‘ ( ◡ 𝑀 ‘ 𝐶 ) ) 𝑅 ( 𝑀 ‘ 𝐵 ) ) )
54	46 53	mpbird	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 )
55		epelg	⊢ ( 𝐵 ∈ dom 𝑀 → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( ◡ 𝑀 ‘ 𝐶 ) ∈ 𝐵 ) )
56	51 55	syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑀 ‘ 𝐶 ) E 𝐵 ↔ ( ◡ 𝑀 ‘ 𝐶 ) ∈ 𝐵 ) )
57	54 56	mpbid	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) ∈ 𝐵 )
58		ffn	⊢ ( ◡ 𝑀 : 𝑋 ⟶ dom 𝑀 → ◡ 𝑀 Fn 𝑋 )
59		elpreima	⊢ ( ◡ 𝑀 Fn 𝑋 → ( 𝐶 ∈ ( ◡ ◡ 𝑀 “ 𝐵 ) ↔ ( 𝐶 ∈ 𝑋 ∧ ( ◡ 𝑀 ‘ 𝐶 ) ∈ 𝐵 ) ) )
60	49 58 59	3syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 ∈ ( ◡ ◡ 𝑀 “ 𝐵 ) ↔ ( 𝐶 ∈ 𝑋 ∧ ( ◡ 𝑀 ‘ 𝐶 ) ∈ 𝐵 ) ) )
61	18 57 60	mpbir2and	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ ( ◡ ◡ 𝑀 “ 𝐵 ) )
62		imacnvcnv	⊢ ( ◡ ◡ 𝑀 “ 𝐵 ) = ( 𝑀 “ 𝐵 )
63	61 62	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ ( 𝑀 “ 𝐵 ) )
64	10	adantr	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 ↾ 𝐵 ) = ( 𝑁 ↾ 𝐵 ) )
65	64	rneqd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ran ( 𝑀 ↾ 𝐵 ) = ran ( 𝑁 ↾ 𝐵 ) )
66		df-ima	⊢ ( 𝑀 “ 𝐵 ) = ran ( 𝑀 ↾ 𝐵 )
67		df-ima	⊢ ( 𝑁 “ 𝐵 ) = ran ( 𝑁 ↾ 𝐵 )
68	65 66 67	3eqtr4g	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝑀 “ 𝐵 ) = ( 𝑁 “ 𝐵 ) )
69	63 68	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ ( 𝑁 “ 𝐵 ) )
70	34 69	sseldd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → 𝐶 ∈ 𝑌 )
71	64	cnveqd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ ( 𝑀 ↾ 𝐵 ) = ◡ ( 𝑁 ↾ 𝐵 ) )
72		dff1o3	⊢ ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 ↔ ( 𝑀 : dom 𝑀 –onto→ 𝑋 ∧ Fun ◡ 𝑀 ) )
73	72	simprbi	⊢ ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 → Fun ◡ 𝑀 )
74		funcnvres	⊢ ( Fun ◡ 𝑀 → ◡ ( 𝑀 ↾ 𝐵 ) = ( ◡ 𝑀 ↾ ( 𝑀 “ 𝐵 ) ) )
75	42 73 74	3syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ ( 𝑀 ↾ 𝐵 ) = ( ◡ 𝑀 ↾ ( 𝑀 “ 𝐵 ) ) )
76		dff1o3	⊢ ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 ↔ ( 𝑁 : dom 𝑁 –onto→ 𝑌 ∧ Fun ◡ 𝑁 ) )
77	76	simprbi	⊢ ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 → Fun ◡ 𝑁 )
78		funcnvres	⊢ ( Fun ◡ 𝑁 → ◡ ( 𝑁 ↾ 𝐵 ) = ( ◡ 𝑁 ↾ ( 𝑁 “ 𝐵 ) ) )
79	30 77 78	3syl	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ◡ ( 𝑁 ↾ 𝐵 ) = ( ◡ 𝑁 ↾ ( 𝑁 “ 𝐵 ) ) )
80	71 75 79	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ↾ ( 𝑀 “ 𝐵 ) ) = ( ◡ 𝑁 ↾ ( 𝑁 “ 𝐵 ) ) )
81	80	fveq1d	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑀 ↾ ( 𝑀 “ 𝐵 ) ) ‘ 𝐶 ) = ( ( ◡ 𝑁 ↾ ( 𝑁 “ 𝐵 ) ) ‘ 𝐶 ) )
82	63	fvresd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑀 ↾ ( 𝑀 “ 𝐵 ) ) ‘ 𝐶 ) = ( ◡ 𝑀 ‘ 𝐶 ) )
83	69	fvresd	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ( ◡ 𝑁 ↾ ( 𝑁 “ 𝐵 ) ) ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) )
84	81 82 83	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) )
85	18 70 84	3jca	⊢ ( ( 𝜑 ∧ 𝐶 𝑅 ( 𝑀 ‘ 𝐵 ) ) → ( 𝐶 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌 ∧ ( ◡ 𝑀 ‘ 𝐶 ) = ( ◡ 𝑁 ‘ 𝐶 ) ) )