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

Theorem fpwwe2lem9 9404
Description: Lemma for fpwwe2 9409. 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 5205 . . . . . . . . . 10 Rel 𝑊
43brrelexi 5118 . . . . . . . . 9 (𝑋𝑊𝑅𝑋 ∈ V)
51, 4syl 17 . . . . . . . 8 (𝜑𝑋 ∈ V)
6 fpwwe2.2 . . . . . . . . . . . 12 (𝜑𝐴 ∈ V)
72, 6fpwwe2lem2 9398 . . . . . . . . . . 11 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
81, 7mpbid 222 . . . . . . . . . 10 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
98simprd 479 . . . . . . . . 9 (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
109simpld 475 . . . . . . . 8 (𝜑𝑅 We 𝑋)
11 fpwwe2lem9.m . . . . . . . . 9 𝑀 = OrdIso(𝑅, 𝑋)
1211oiiso 8386 . . . . . . . 8 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
135, 10, 12syl2anc 692 . . . . . . 7 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
14 isof1o 6527 . . . . . . 7 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
1513, 14syl 17 . . . . . 6 (𝜑𝑀:dom 𝑀1-1-onto𝑋)
16 f1ofo 6101 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋𝑀:dom 𝑀onto𝑋)
17 forn 6075 . . . . . 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 9403 . . . . . 6 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
2423rneqd 5313 . . . . 5 (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀))
2518, 24eqtr3d 2657 . . . 4 (𝜑𝑋 = ran (𝑁 ↾ dom 𝑀))
26 df-ima 5087 . . . 4 (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀)
2725, 26syl6eqr 2673 . . 3 (𝜑𝑋 = (𝑁 “ dom 𝑀))
28 imassrn 5436 . . . 4 (𝑁 “ dom 𝑀) ⊆ ran 𝑁
293brrelexi 5118 . . . . . . . 8 (𝑌𝑊𝑆𝑌 ∈ V)
3020, 29syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
312, 6fpwwe2lem2 9398 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
3220, 31mpbid 222 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
3332simprd 479 . . . . . . . 8 (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))
3433simpld 475 . . . . . . 7 (𝜑𝑆 We 𝑌)
3521oiiso 8386 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
3630, 34, 35syl2anc 692 . . . . . 6 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
37 isof1o 6527 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
3836, 37syl 17 . . . . 5 (𝜑𝑁:dom 𝑁1-1-onto𝑌)
39 f1ofo 6101 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
40 forn 6075 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
4138, 39, 403syl 18 . . . 4 (𝜑 → ran 𝑁 = 𝑌)
4228, 41syl5sseq 3632 . . 3 (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌)
4327, 42eqsstrd 3618 . 2 (𝜑𝑋𝑌)
448simpld 475 . . . . . 6 (𝜑 → (𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)))
4544simprd 479 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
46 relxp 5188 . . . . 5 Rel (𝑋 × 𝑋)
47 relss 5167 . . . . 5 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
4845, 46, 47mpisyl 21 . . . 4 (𝜑 → Rel 𝑅)
49 inss2 3812 . . . . 5 (𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋)
50 relxp 5188 . . . . 5 Rel (𝑌 × 𝑋)
51 relss 5167 . . . . 5 ((𝑆 ∩ (𝑌 × 𝑋)) ⊆ (𝑌 × 𝑋) → (Rel (𝑌 × 𝑋) → Rel (𝑆 ∩ (𝑌 × 𝑋))))
5249, 50, 51mp2 9 . . . 4 Rel (𝑆 ∩ (𝑌 × 𝑋))
5348, 52jctir 560 . . 3 (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))))
5445ssbrd 4656 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑥(𝑋 × 𝑋)𝑦))
55 brxp 5107 . . . . . . 7 (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥𝑋𝑦𝑋))
5654, 55syl6ib 241 . . . . . 6 (𝜑 → (𝑥𝑅𝑦 → (𝑥𝑋𝑦𝑋)))
57 brinxp2 5141 . . . . . . . 8 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ (𝑥𝑌𝑦𝑋𝑥𝑆𝑦))
58 df-3an 1038 . . . . . . . 8 ((𝑥𝑌𝑦𝑋𝑥𝑆𝑦) ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
5957, 58bitri 264 . . . . . . 7 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
60 simprll 801 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑌)
61 simprr 795 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦)
62 isocnv 6534 . . . . . . . . . . . . . . . . 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 802 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑋)
6765, 66sseldd 3584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑌)
68 isorel 6530 . . . . . . . . . . . . . . 15 ((𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥𝑌𝑦𝑌)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6964, 60, 67, 68syl12anc 1321 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
7061, 69mpbid 222 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) E (𝑁𝑦))
71 fvex 6158 . . . . . . . . . . . . . 14 (𝑁𝑦) ∈ V
7271epelc 4987 . . . . . . . . . . . . 13 ((𝑁𝑥) E (𝑁𝑦) ↔ (𝑁𝑥) ∈ (𝑁𝑦))
7370, 72sylib 208 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ (𝑁𝑦))
7423adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
7574cnveqd 5258 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
76 isof1o 6527 . . . . . . . . . . . . . . . . . 18 (𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → 𝑁:𝑌1-1-onto→dom 𝑁)
77 f1ofn 6095 . . . . . . . . . . . . . . . . . 18 (𝑁:𝑌1-1-onto→dom 𝑁𝑁 Fn 𝑌)
7864, 76, 773syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Fn 𝑌)
79 fnfun 5946 . . . . . . . . . . . . . . . . 17 (𝑁 Fn 𝑌 → Fun 𝑁)
80 funcnvres 5925 . . . . . . . . . . . . . . . . 17 (Fun 𝑁(𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8178, 79, 803syl 18 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8275, 81eqtrd 2655 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ (𝑁 “ dom 𝑀)))
8382fveq1d 6150 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦))
8427adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
8566, 84eleqtrd 2700 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
86 fvres 6164 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑁 “ dom 𝑀) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
8785, 86syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
8883, 87eqtrd 2655 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = (𝑁𝑦))
89 isocnv 6534 . . . . . . . . . . . . . . . . 17 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
9013, 89syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
91 isof1o 6527 . . . . . . . . . . . . . . . 16 (𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → 𝑀:𝑋1-1-onto→dom 𝑀)
92 f1of 6094 . . . . . . . . . . . . . . . 16 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
9390, 91, 923syl 18 . . . . . . . . . . . . . . 15 (𝜑𝑀:𝑋⟶dom 𝑀)
9493adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀:𝑋⟶dom 𝑀)
9594, 66ffvelrnd 6316 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) ∈ dom 𝑀)
9688, 95eqeltrrd 2699 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑦) ∈ dom 𝑀)
9711oicl 8378 . . . . . . . . . . . . 13 Ord dom 𝑀
98 ordtr1 5726 . . . . . . . . . . . . 13 (Ord dom 𝑀 → (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀))
9997, 98ax-mp 5 . . . . . . . . . . . 12 (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀)
10073, 96, 99syl2anc 692 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ dom 𝑀)
101 elpreima 6293 . . . . . . . . . . . 12 (𝑁 Fn 𝑌 → (𝑥 ∈ (𝑁 “ dom 𝑀) ↔ (𝑥𝑌 ∧ (𝑁𝑥) ∈ dom 𝑀)))
10278, 101syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥 ∈ (𝑁 “ dom 𝑀) ↔ (𝑥𝑌 ∧ (𝑁𝑥) ∈ dom 𝑀)))
10360, 100, 102mpbir2and 956 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
104 imacnvcnv 5558 . . . . . . . . . . 11 (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)
10584, 104syl6eqr 2673 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
106103, 105eleqtrrd 2701 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑋)
107106, 66jca 554 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑋𝑦𝑋))
108107ex 450 . . . . . . 7 (𝜑 → (((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦) → (𝑥𝑋𝑦𝑋)))
10959, 108syl5bi 232 . . . . . 6 (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥𝑋𝑦𝑋)))
11023adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
111110cnveqd 5258 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
112111fveq1d 6150 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑥) = ((𝑁 ↾ dom 𝑀)‘𝑥))
113111fveq1d 6150 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑦) = ((𝑁 ↾ dom 𝑀)‘𝑦))
114112, 113breq12d 4626 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑀𝑥) E (𝑀𝑦) ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
115 isorel 6530 . . . . . . . . . 10 ((𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
11690, 115sylan 488 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
117 eqidd 2622 . . . . . . . . . . . . 13 (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀))
118 isores3 6539 . . . . . . . . . . . . 13 ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
11936, 22, 117, 118syl3anc 1323 . . . . . . . . . . . 12 (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
120 isocnv 6534 . . . . . . . . . . . 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 793 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
12427adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑋 = (𝑁 “ dom 𝑀))
125123, 124eleqtrd 2700 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
126 simprr 795 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
127126, 124eleqtrd 2700 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
128 isorel 6530 . . . . . . . . . 10 (((𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
129122, 125, 127, 128syl12anc 1321 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
130114, 116, 1293bitr4d 300 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥𝑆𝑦))
13143sselda 3583 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑌)
132131adantrr 752 . . . . . . . . . . 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 4614 . . . . 5 (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
140 df-br 4614 . . . . 5 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋)))
141138, 139, 1403bitr3g 302 . . . 4 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋))))
142141eqrelrdv2 5180 . . 3 (((Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
14353, 142mpancom 702 . 2 (𝜑𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
14443, 143jca 554 1 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  [wsbc 3417  cin 3554  wss 3555  {csn 4148  cop 4154   class class class wbr 4613  {copab 4672   E cep 4983   We wwe 5032   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Rel wrel 5079  Ord word 5681  Fun wfun 5841   Fn wfn 5842  wf 5843  ontowfo 5845  1-1-ontowf1o 5846  cfv 5847   Isom wiso 5848  (class class class)co 6604  OrdIsocoi 8358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-wrecs 7352  df-recs 7413  df-oi 8359
This theorem is referenced by:  fpwwe2lem10  9405
  Copyright terms: Public domain W3C validator