fpwwe2lem8

Description: Lemma for fpwwe2 . Given two well-orders <. X , R >. and <. Y , S >. of parts of A , one is an initial segment of the other. (The O C_ P hypothesis is in order to break the symmetry of X and Y .) (Contributed by Mario Carneiro, 15-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022) (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 ( 𝑆 , 𝑌 )
	fpwwe2lem8.s	⊢ ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
Assertion	fpwwe2lem8	⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )

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		fpwwe2lem8.s	⊢ ( 𝜑 → dom 𝑀 ⊆ dom 𝑁 )
9	1	relopabiv	⊢ Rel 𝑊
10	9	brrelex1i	⊢ ( 𝑋 𝑊 𝑅 → 𝑋 ∈ V )
11	4 10	syl	⊢ ( 𝜑 → 𝑋 ∈ V )
12	1 2	fpwwe2lem2	⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ^◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
13	4 12	mpbid	⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ^◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
14	13	simprld	⊢ ( 𝜑 → 𝑅 We 𝑋 )
15	6	oiiso	⊢ ( ( 𝑋 ∈ V ∧ 𝑅 We 𝑋 ) → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
16	11 14 15	syl2anc	⊢ ( 𝜑 → 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) )
17		isof1o	⊢ ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 )
18		f1ofo	⊢ ( 𝑀 : dom 𝑀 –1-1-onto→ 𝑋 → 𝑀 : dom 𝑀 –onto→ 𝑋 )
19		forn	⊢ ( 𝑀 : dom 𝑀 –onto→ 𝑋 → ran 𝑀 = 𝑋 )
20	16 17 18 19	4syl	⊢ ( 𝜑 → ran 𝑀 = 𝑋 )
21	1 2 3 4 5 6 7 8	fpwwe2lem7	⊢ ( 𝜑 → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
22	21	rneqd	⊢ ( 𝜑 → ran 𝑀 = ran ( 𝑁 ↾ dom 𝑀 ) )
23	20 22	eqtr3d	⊢ ( 𝜑 → 𝑋 = ran ( 𝑁 ↾ dom 𝑀 ) )
24		df-ima	⊢ ( 𝑁 “ dom 𝑀 ) = ran ( 𝑁 ↾ dom 𝑀 )
25	23 24	eqtr4di	⊢ ( 𝜑 → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
26		imassrn	⊢ ( 𝑁 “ dom 𝑀 ) ⊆ ran 𝑁
27	9	brrelex1i	⊢ ( 𝑌 𝑊 𝑆 → 𝑌 ∈ V )
28	5 27	syl	⊢ ( 𝜑 → 𝑌 ∈ V )
29	1 2	fpwwe2lem2	⊢ ( 𝜑 → ( 𝑌 𝑊 𝑆 ↔ ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ^◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
30	5 29	mpbid	⊢ ( 𝜑 → ( ( 𝑌 ⊆ 𝐴 ∧ 𝑆 ⊆ ( 𝑌 × 𝑌 ) ) ∧ ( 𝑆 We 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 [ ( ^◡ 𝑆 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑆 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
31	30	simprld	⊢ ( 𝜑 → 𝑆 We 𝑌 )
32	7	oiiso	⊢ ( ( 𝑌 ∈ V ∧ 𝑆 We 𝑌 ) → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
33	28 31 32	syl2anc	⊢ ( 𝜑 → 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) )
34		isof1o	⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 )
35		f1ofo	⊢ ( 𝑁 : dom 𝑁 –1-1-onto→ 𝑌 → 𝑁 : dom 𝑁 –onto→ 𝑌 )
36		forn	⊢ ( 𝑁 : dom 𝑁 –onto→ 𝑌 → ran 𝑁 = 𝑌 )
37	33 34 35 36	4syl	⊢ ( 𝜑 → ran 𝑁 = 𝑌 )
38	26 37	sseqtrid	⊢ ( 𝜑 → ( 𝑁 “ dom 𝑀 ) ⊆ 𝑌 )
39	25 38	eqsstrd	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
40	13	simplrd	⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑋 × 𝑋 ) )
41		relxp	⊢ Rel ( 𝑋 × 𝑋 )
42		relss	⊢ ( 𝑅 ⊆ ( 𝑋 × 𝑋 ) → ( Rel ( 𝑋 × 𝑋 ) → Rel 𝑅 ) )
43	40 41 42	mpisyl	⊢ ( 𝜑 → Rel 𝑅 )
44		relinxp	⊢ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) )
45	43 44	jctir	⊢ ( 𝜑 → ( Rel 𝑅 ∧ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
46	40	ssbrd	⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ) )
47		brxp	⊢ ( 𝑥 ( 𝑋 × 𝑋 ) 𝑦 ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
48	46 47	imbitrdi	⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
49		brinxp2	⊢ ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) )
50		isocnv	⊢ ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) → ^◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
51	33 50	syl	⊢ ( 𝜑 → ^◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) )
53		isof1o	⊢ ( ^◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) → ^◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 )
54		f1ofn	⊢ ( ^◡ 𝑁 : 𝑌 –1-1-onto→ dom 𝑁 → ^◡ 𝑁 Fn 𝑌 )
55	52 53 54	3syl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ 𝑁 Fn 𝑌 )
56		simprll	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ 𝑌 )
57		simprr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 𝑆 𝑦 )
58	39	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 ⊆ 𝑌 )
59		simprlr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ 𝑋 )
60	58 59	sseldd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ 𝑌 )
61		isorel	⊢ ( ( ^◡ 𝑁 Isom 𝑆 , E ( 𝑌 , dom 𝑁 ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ^◡ 𝑁 ‘ 𝑥 ) E ( ^◡ 𝑁 ‘ 𝑦 ) ) )
62	52 56 60 61	syl12anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ^◡ 𝑁 ‘ 𝑥 ) E ( ^◡ 𝑁 ‘ 𝑦 ) ) )
63	57 62	mpbid	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑁 ‘ 𝑥 ) E ( ^◡ 𝑁 ‘ 𝑦 ) )
64		fvex	⊢ ( ^◡ 𝑁 ‘ 𝑦 ) ∈ V
65	64	epeli	⊢ ( ( ^◡ 𝑁 ‘ 𝑥 ) E ( ^◡ 𝑁 ‘ 𝑦 ) ↔ ( ^◡ 𝑁 ‘ 𝑥 ) ∈ ( ^◡ 𝑁 ‘ 𝑦 ) )
66	63 65	sylib	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑁 ‘ 𝑥 ) ∈ ( ^◡ 𝑁 ‘ 𝑦 ) )
67	21	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
68	67	cnveqd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ 𝑀 = ^◡ ( 𝑁 ↾ dom 𝑀 ) )
69		fnfun	⊢ ( ^◡ 𝑁 Fn 𝑌 → Fun ^◡ 𝑁 )
70		funcnvres	⊢ ( Fun ^◡ 𝑁 → ^◡ ( 𝑁 ↾ dom 𝑀 ) = ( ^◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
71	55 69 70	3syl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ ( 𝑁 ↾ dom 𝑀 ) = ( ^◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
72	68 71	eqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ 𝑀 = ( ^◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) )
73	72	fveq1d	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑀 ‘ 𝑦 ) = ( ( ^◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) ‘ 𝑦 ) )
74	25	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
75	59 74	eleqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) )
76	75	fvresd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ( ^◡ 𝑁 ↾ ( 𝑁 “ dom 𝑀 ) ) ‘ 𝑦 ) = ( ^◡ 𝑁 ‘ 𝑦 ) )
77	73 76	eqtrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑀 ‘ 𝑦 ) = ( ^◡ 𝑁 ‘ 𝑦 ) )
78		isocnv	⊢ ( 𝑀 Isom E , 𝑅 ( dom 𝑀 , 𝑋 ) → ^◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
79		isof1o	⊢ ( ^◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) → ^◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 )
80		f1of	⊢ ( ^◡ 𝑀 : 𝑋 –1-1-onto→ dom 𝑀 → ^◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
81	16 78 79 80	4syl	⊢ ( 𝜑 → ^◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
82	81	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ^◡ 𝑀 : 𝑋 ⟶ dom 𝑀 )
83	82 59	ffvelcdmd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑀 ‘ 𝑦 ) ∈ dom 𝑀 )
84	77 83	eqeltrrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑁 ‘ 𝑦 ) ∈ dom 𝑀 )
85	6	oicl	⊢ Ord dom 𝑀
86		ordtr1	⊢ ( Ord dom 𝑀 → ( ( ( ^◡ 𝑁 ‘ 𝑥 ) ∈ ( ^◡ 𝑁 ‘ 𝑦 ) ∧ ( ^◡ 𝑁 ‘ 𝑦 ) ∈ dom 𝑀 ) → ( ^◡ 𝑁 ‘ 𝑥 ) ∈ dom 𝑀 ) )
87	85 86	ax-mp	⊢ ( ( ( ^◡ 𝑁 ‘ 𝑥 ) ∈ ( ^◡ 𝑁 ‘ 𝑦 ) ∧ ( ^◡ 𝑁 ‘ 𝑦 ) ∈ dom 𝑀 ) → ( ^◡ 𝑁 ‘ 𝑥 ) ∈ dom 𝑀 )
88	66 84 87	syl2anc	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( ^◡ 𝑁 ‘ 𝑥 ) ∈ dom 𝑀 )
89	55 56 88	elpreimad	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ ( ^◡ ^◡ 𝑁 “ dom 𝑀 ) )
90		imacnvcnv	⊢ ( ^◡ ^◡ 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 )
91	74 90	eqtr4di	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑋 = ( ^◡ ^◡ 𝑁 “ dom 𝑀 ) )
92	89 91	eleqtrrd	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → 𝑥 ∈ 𝑋 )
93	92 59	jca	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
94	93	ex	⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
95	49 94	biimtrid	⊢ ( 𝜑 → ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
96	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑀 = ( 𝑁 ↾ dom 𝑀 ) )
97	96	cnveqd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ^◡ 𝑀 = ^◡ ( 𝑁 ↾ dom 𝑀 ) )
98	97	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ^◡ 𝑀 ‘ 𝑥 ) = ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) )
99	97	fveq1d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ^◡ 𝑀 ‘ 𝑦 ) = ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) )
100	98 99	breq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ^◡ 𝑀 ‘ 𝑥 ) E ( ^◡ 𝑀 ‘ 𝑦 ) ↔ ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
101	16 78	syl	⊢ ( 𝜑 → ^◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) )
102		isorel	⊢ ( ( ^◡ 𝑀 Isom 𝑅 , E ( 𝑋 , dom 𝑀 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ^◡ 𝑀 ‘ 𝑥 ) E ( ^◡ 𝑀 ‘ 𝑦 ) ) )
103	101 102	sylan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ^◡ 𝑀 ‘ 𝑥 ) E ( ^◡ 𝑀 ‘ 𝑦 ) ) )
104		eqidd	⊢ ( 𝜑 → ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) )
105		isores3	⊢ ( ( 𝑁 Isom E , 𝑆 ( dom 𝑁 , 𝑌 ) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ ( 𝑁 “ dom 𝑀 ) = ( 𝑁 “ dom 𝑀 ) ) → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
106	33 8 104 105	syl3anc	⊢ ( 𝜑 → ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) )
107		isocnv	⊢ ( ( 𝑁 ↾ dom 𝑀 ) Isom E , 𝑆 ( dom 𝑀 , ( 𝑁 “ dom 𝑀 ) ) → ^◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
108	106 107	syl	⊢ ( 𝜑 → ^◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
109	108	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ^◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) )
110		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
111	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 = ( 𝑁 “ dom 𝑀 ) )
112	110 111	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) )
113		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
114	113 111	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) )
115		isorel	⊢ ( ( ^◡ ( 𝑁 ↾ dom 𝑀 ) Isom 𝑆 , E ( ( 𝑁 “ dom 𝑀 ) , dom 𝑀 ) ∧ ( 𝑥 ∈ ( 𝑁 “ dom 𝑀 ) ∧ 𝑦 ∈ ( 𝑁 “ dom 𝑀 ) ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
116	109 112 114 115	syl12anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑥 ) E ( ^◡ ( 𝑁 ↾ dom 𝑀 ) ‘ 𝑦 ) ) )
117	100 103 116	3bitr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑆 𝑦 ) )
118	39	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑌 )
119	118	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑌 )
120	119 113	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) )
121	120	biantrurd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋 ) ∧ 𝑥 𝑆 𝑦 ) ) )
122	121 49	bitr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑆 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
123	117 122	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
124	123	ex	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) ) )
125	48 95 124	pm5.21ndd	⊢ ( 𝜑 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ) )
126		df-br	⊢ ( 𝑥 𝑅 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 )
127		df-br	⊢ ( 𝑥 ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
128	125 126 127	3bitr3g	⊢ ( 𝜑 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )
129	128	eqrelrdv2	⊢ ( ( ( Rel 𝑅 ∧ Rel ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) ∧ 𝜑 ) → 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
130	45 129	mpancom	⊢ ( 𝜑 → 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) )
131	39 130	jca	⊢ ( 𝜑 → ( 𝑋 ⊆ 𝑌 ∧ 𝑅 = ( 𝑆 ∩ ( 𝑌 × 𝑋 ) ) ) )

Metamath Proof Explorer

Theorem fpwwe2lem8

Proof