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

Theorem fpwwe2lem9 9457
Description: Lemma for fpwwe2 9462. Given two well-orders 𝑋, 𝑅 and 𝑌, 𝑆 of parts of 𝐴, one is an initial segment of the other. (The 𝑂𝑃 hypothesis is in order to break the symmetry of 𝑋 and 𝑌.) (Contributed by Mario Carneiro, 15-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2lem9.x (𝜑𝑋𝑊𝑅)
fpwwe2lem9.y (𝜑𝑌𝑊𝑆)
fpwwe2lem9.m 𝑀 = OrdIso(𝑅, 𝑋)
fpwwe2lem9.n 𝑁 = OrdIso(𝑆, 𝑌)
fpwwe2lem9.s (𝜑 → dom 𝑀 ⊆ dom 𝑁)
Assertion
Ref Expression
fpwwe2lem9 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)

Proof of Theorem fpwwe2lem9
StepHypRef Expression
1 fpwwe2lem9.x . . . . . . . . 9 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . . . . 11 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
32relopabi 5243 . . . . . . . . . 10 Rel 𝑊
43brrelexi 5156 . . . . . . . . 9 (𝑋𝑊𝑅𝑋 ∈ V)
51, 4syl 17 . . . . . . . 8 (𝜑𝑋 ∈ V)
6 fpwwe2.2 . . . . . . . . . . . 12 (𝜑𝐴 ∈ V)
72, 6fpwwe2lem2 9451 . . . . . . . . . . 11 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
81, 7mpbid 222 . . . . . . . . . 10 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
98simprd 479 . . . . . . . . 9 (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
109simpld 475 . . . . . . . 8 (𝜑𝑅 We 𝑋)
11 fpwwe2lem9.m . . . . . . . . 9 𝑀 = OrdIso(𝑅, 𝑋)
1211oiiso 8439 . . . . . . . 8 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
135, 10, 12syl2anc 693 . . . . . . 7 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
14 isof1o 6570 . . . . . . 7 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
1513, 14syl 17 . . . . . 6 (𝜑𝑀:dom 𝑀1-1-onto𝑋)
16 f1ofo 6142 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋𝑀:dom 𝑀onto𝑋)
17 forn 6116 . . . . . 6 (𝑀:dom 𝑀onto𝑋 → ran 𝑀 = 𝑋)
1815, 16, 173syl 18 . . . . 5 (𝜑 → ran 𝑀 = 𝑋)
19 fpwwe2.3 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
20 fpwwe2lem9.y . . . . . . 7 (𝜑𝑌𝑊𝑆)
21 fpwwe2lem9.n . . . . . . 7 𝑁 = OrdIso(𝑆, 𝑌)
22 fpwwe2lem9.s . . . . . . 7 (𝜑 → dom 𝑀 ⊆ dom 𝑁)
232, 6, 19, 1, 20, 11, 21, 22fpwwe2lem8 9456 . . . . . 6 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
2423rneqd 5351 . . . . 5 (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀))
2518, 24eqtr3d 2657 . . . 4 (𝜑𝑋 = ran (𝑁 ↾ dom 𝑀))
26 df-ima 5125 . . . 4 (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀)
2725, 26syl6eqr 2673 . . 3 (𝜑𝑋 = (𝑁 “ dom 𝑀))
28 imassrn 5475 . . . 4 (𝑁 “ dom 𝑀) ⊆ ran 𝑁
293brrelexi 5156 . . . . . . . 8 (𝑌𝑊𝑆𝑌 ∈ V)
3020, 29syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
312, 6fpwwe2lem2 9451 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
3220, 31mpbid 222 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
3332simprd 479 . . . . . . . 8 (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))
3433simpld 475 . . . . . . 7 (𝜑𝑆 We 𝑌)
3521oiiso 8439 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
3630, 34, 35syl2anc 693 . . . . . 6 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
37 isof1o 6570 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
3836, 37syl 17 . . . . 5 (𝜑𝑁:dom 𝑁1-1-onto𝑌)
39 f1ofo 6142 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
40 forn 6116 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
4138, 39, 403syl 18 . . . 4 (𝜑 → ran 𝑁 = 𝑌)
4228, 41syl5sseq 3651 . . 3 (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌)
4327, 42eqsstrd 3637 . 2 (𝜑𝑋𝑌)
448simpld 475 . . . . . 6 (𝜑 → (𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)))
4544simprd 479 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
46 relxp 5225 . . . . 5 Rel (𝑋 × 𝑋)
47 relss 5204 . . . . 5 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
4845, 46, 47mpisyl 21 . . . 4 (𝜑 → Rel 𝑅)
49 inss2 3832 . . . . 5 (𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋)
50 relxp 5225 . . . . 5 Rel (𝑌 × 𝑋)
51 relss 5204 . . . . 5 ((𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋) → (Rel (𝑌 × 𝑋) → Rel (𝑆 ∩ (𝑌 × 𝑋))))
5249, 50, 51mp2 9 . . . 4 Rel (𝑆 ∩ (𝑌 × 𝑋))
5348, 52jctir 561 . . 3 (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))))
5445ssbrd 4694 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑥(𝑋 × 𝑋)𝑦))
55 brxp 5145 . . . . . . 7 (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥𝑋𝑦𝑋))
5654, 55syl6ib 241 . . . . . 6 (𝜑 → (𝑥𝑅𝑦 → (𝑥𝑋𝑦𝑋)))
57 brinxp2 5178 . . . . . . . 8 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ (𝑥𝑌𝑦𝑋𝑥𝑆𝑦))
58 df-3an 1039 . . . . . . . 8 ((𝑥𝑌𝑦𝑋𝑥𝑆𝑦) ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
5957, 58bitri 264 . . . . . . 7 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
60 simprll 802 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑌)
61 simprr 796 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦)
62 isocnv 6577 . . . . . . . . . . . . . . . . 17 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
6336, 62syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
6463adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
6543adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋𝑌)
66 simprlr 803 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑋)
6765, 66sseldd 3602 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑌)
68 isorel 6573 . . . . . . . . . . . . . . 15 ((𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥𝑌𝑦𝑌)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6964, 60, 67, 68syl12anc 1323 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
7061, 69mpbid 222 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) E (𝑁𝑦))
71 fvex 6199 . . . . . . . . . . . . . 14 (𝑁𝑦) ∈ V
7271epelc 5029 . . . . . . . . . . . . 13 ((𝑁𝑥) E (𝑁𝑦) ↔ (𝑁𝑥) ∈ (𝑁𝑦))
7370, 72sylib 208 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ (𝑁𝑦))
7423adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
7574cnveqd 5296 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
76 isof1o 6570 . . . . . . . . . . . . . . . . . 18 (𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → 𝑁:𝑌1-1-onto→dom 𝑁)
77 f1ofn 6136 . . . . . . . . . . . . . . . . . 18 (𝑁:𝑌1-1-onto→dom 𝑁𝑁 Fn 𝑌)
7864, 76, 773syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Fn 𝑌)
79 fnfun 5986 . . . . . . . . . . . . . . . . 17 (𝑁 Fn 𝑌 → Fun 𝑁)
80 funcnvres 5965 . . . . . . . . . . . . . . . . 17 (Fun 𝑁(𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8178, 79, 803syl 18 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8275, 81eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8382fveq1d 6191 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦))
8427adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
8566, 84eleqtrd 2702 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
86 fvres 6205 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑁 “ dom 𝑀) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
8785, 86syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
8883, 87eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = (𝑁𝑦))
89 isocnv 6577 . . . . . . . . . . . . . . . . 17 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
9013, 89syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
91 isof1o 6570 . . . . . . . . . . . . . . . 16 (𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → 𝑀:𝑋1-1-onto→dom 𝑀)
92 f1of 6135 . . . . . . . . . . . . . . . 16 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
9390, 91, 923syl 18 . . . . . . . . . . . . . . 15 (𝜑𝑀:𝑋⟶dom 𝑀)
9493adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀:𝑋⟶dom 𝑀)
9594, 66ffvelrnd 6358 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) ∈ dom 𝑀)
9688, 95eqeltrrd 2701 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑦) ∈ dom 𝑀)
9711oicl 8431 . . . . . . . . . . . . 13 Ord dom 𝑀
98 ordtr1 5765 . . . . . . . . . . . . 13 (Ord dom 𝑀 → (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀))
9997, 98ax-mp 5 . . . . . . . . . . . 12 (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀)
10073, 96, 99syl2anc 693 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ dom 𝑀)
101 elpreima 6335 . . . . . . . . . . . 12 (𝑁 Fn 𝑌 → (𝑥 ∈ (𝑁 “ dom 𝑀) ↔ (𝑥𝑌 ∧ (𝑁𝑥) ∈ dom 𝑀)))
10278, 101syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ (𝑁 “ dom 𝑀) ↔ (𝑥𝑌 ∧ (𝑁𝑥) ∈ dom 𝑀)))
10360, 100, 102mpbir2and 957 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
104 imacnvcnv 5597 . . . . . . . . . . 11 (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)
10584, 104syl6eqr 2673 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
106103, 105eleqtrrd 2703 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑋)
107106, 66jca 554 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑋𝑦𝑋))
108107ex 450 . . . . . . 7 (𝜑 → (((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦) → (𝑥𝑋𝑦𝑋)))
10959, 108syl5bi 232 . . . . . 6 (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥𝑋𝑦𝑋)))
11023adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
111110cnveqd 5296 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
112111fveq1d 6191 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑥) = ((𝑁 ↾ dom 𝑀)‘𝑥))
113111fveq1d 6191 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑦) = ((𝑁 ↾ dom 𝑀)‘𝑦))
114112, 113breq12d 4664 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑀𝑥) E (𝑀𝑦) ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
115 isorel 6573 . . . . . . . . . 10 ((𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
11690, 115sylan 488 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
117 eqidd 2622 . . . . . . . . . . . . 13 (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀))
118 isores3 6582 . . . . . . . . . . . . 13 ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
11936, 22, 117, 118syl3anc 1325 . . . . . . . . . . . 12 (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
120 isocnv 6577 . . . . . . . . . . . 12 ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
121119, 120syl 17 . . . . . . . . . . 11 (𝜑(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
122121adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
123 simprl 794 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
12427adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑋 = (𝑁 “ dom 𝑀))
125123, 124eleqtrd 2702 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
126 simprr 796 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
127126, 124eleqtrd 2702 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
128 isorel 6573 . . . . . . . . . 10 (((𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
129122, 125, 127, 128syl12anc 1323 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
130114, 116, 1293bitr4d 300 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥𝑆𝑦))
13143sselda 3601 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑌)
132131adantrr 753 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑌)
133132, 126jca 554 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑌𝑦𝑋))
134133biantrurd 529 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)))
135134, 59syl6bbr 278 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
136130, 135bitrd 268 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
137136ex 450 . . . . . 6 (𝜑 → ((𝑥𝑋𝑦𝑋) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)))
13856, 109, 137pm5.21ndd 369 . . . . 5 (𝜑 → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
139 df-br 4652 . . . . 5 (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
140 df-br 4652 . . . . 5 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋)))
141138, 139, 1403bitr3g 302 . . . 4 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋))))
142141eqrelrdv2 5217 . . 3 (((Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
14353, 142mpancom 703 . 2 (𝜑𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
14443, 143jca 554 1 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1037   = wceq 1482  wcel 1989  wral 2911  Vcvv 3198  [wsbc 3433  cin 3571  wss 3572  {csn 4175  cop 4181   class class class wbr 4651  {copab 4710   E cep 5026   We wwe 5070   × cxp 5110  ccnv 5111  dom cdm 5112  ran crn 5113  cres 5114  cima 5115  Rel wrel 5117  Ord word 5720  Fun wfun 5880   Fn wfn 5881  wf 5882  ontowfo 5884  1-1-ontowf1o 5885  cfv 5886   Isom wiso 5887  (class class class)co 6647  OrdIsocoi 8411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-rep 4769  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-ov 6650  df-wrecs 7404  df-recs 7465  df-oi 8412
This theorem is referenced by:  fpwwe2lem10  9458
  Copyright terms: Public domain W3C validator