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

Theorem fpwwe2lem8 10575
Description: Lemma for fpwwe2 10580. 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.) (Proof shortened by Peter Mazsa, 23-Sep-2022.) (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(𝑆, 𝑌)
fpwwe2lem8.s (𝜑 → dom 𝑀 ⊆ dom 𝑁)
Assertion
Ref Expression
fpwwe2lem8 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Distinct variable groups:   𝑦,𝑢,𝑟,𝑥,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)   𝑉(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2lem8
StepHypRef Expression
1 fpwwe2lem8.x . . . . . . . . 9 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . . . . 11 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
32relopabiv 5777 . . . . . . . . . 10 Rel 𝑊
43brrelex1i 5689 . . . . . . . . 9 (𝑋𝑊𝑅𝑋 ∈ V)
51, 4syl 17 . . . . . . . 8 (𝜑𝑋 ∈ V)
6 fpwwe2.2 . . . . . . . . . . 11 (𝜑𝐴𝑉)
72, 6fpwwe2lem2 10569 . . . . . . . . . 10 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
81, 7mpbid 231 . . . . . . . . 9 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
98simprld 771 . . . . . . . 8 (𝜑𝑅 We 𝑋)
10 fpwwe2lem8.m . . . . . . . . 9 𝑀 = OrdIso(𝑅, 𝑋)
1110oiiso 9474 . . . . . . . 8 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
125, 9, 11syl2anc 585 . . . . . . 7 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
13 isof1o 7269 . . . . . . 7 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
1412, 13syl 17 . . . . . 6 (𝜑𝑀:dom 𝑀1-1-onto𝑋)
15 f1ofo 6792 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋𝑀:dom 𝑀onto𝑋)
16 forn 6760 . . . . . 6 (𝑀:dom 𝑀onto𝑋 → ran 𝑀 = 𝑋)
1714, 15, 163syl 18 . . . . 5 (𝜑 → ran 𝑀 = 𝑋)
18 fpwwe2.3 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
19 fpwwe2lem8.y . . . . . . 7 (𝜑𝑌𝑊𝑆)
20 fpwwe2lem8.n . . . . . . 7 𝑁 = OrdIso(𝑆, 𝑌)
21 fpwwe2lem8.s . . . . . . 7 (𝜑 → dom 𝑀 ⊆ dom 𝑁)
222, 6, 18, 1, 19, 10, 20, 21fpwwe2lem7 10574 . . . . . 6 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
2322rneqd 5894 . . . . 5 (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀))
2417, 23eqtr3d 2779 . . . 4 (𝜑𝑋 = ran (𝑁 ↾ dom 𝑀))
25 df-ima 5647 . . . 4 (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀)
2624, 25eqtr4di 2795 . . 3 (𝜑𝑋 = (𝑁 “ dom 𝑀))
27 imassrn 6025 . . . 4 (𝑁 “ dom 𝑀) ⊆ ran 𝑁
283brrelex1i 5689 . . . . . . . 8 (𝑌𝑊𝑆𝑌 ∈ V)
2919, 28syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
302, 6fpwwe2lem2 10569 . . . . . . . . 9 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
3119, 30mpbid 231 . . . . . . . 8 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
3231simprld 771 . . . . . . 7 (𝜑𝑆 We 𝑌)
3320oiiso 9474 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
3429, 32, 33syl2anc 585 . . . . . 6 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
35 isof1o 7269 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
3634, 35syl 17 . . . . 5 (𝜑𝑁:dom 𝑁1-1-onto𝑌)
37 f1ofo 6792 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
38 forn 6760 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
3936, 37, 383syl 18 . . . 4 (𝜑 → ran 𝑁 = 𝑌)
4027, 39sseqtrid 3997 . . 3 (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌)
4126, 40eqsstrd 3983 . 2 (𝜑𝑋𝑌)
428simplrd 769 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
43 relxp 5652 . . . . 5 Rel (𝑋 × 𝑋)
44 relss 5738 . . . . 5 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
4542, 43, 44mpisyl 21 . . . 4 (𝜑 → Rel 𝑅)
46 relinxp 5771 . . . 4 Rel (𝑆 ∩ (𝑌 × 𝑋))
4745, 46jctir 522 . . 3 (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))))
4842ssbrd 5149 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑥(𝑋 × 𝑋)𝑦))
49 brxp 5682 . . . . . . 7 (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥𝑋𝑦𝑋))
5048, 49syl6ib 251 . . . . . 6 (𝜑 → (𝑥𝑅𝑦 → (𝑥𝑋𝑦𝑋)))
51 brinxp2 5710 . . . . . . 7 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
52 isocnv 7276 . . . . . . . . . . . . . 14 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5334, 52syl 17 . . . . . . . . . . . . 13 (𝜑𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5453adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
55 isof1o 7269 . . . . . . . . . . . 12 (𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → 𝑁:𝑌1-1-onto→dom 𝑁)
56 f1ofn 6786 . . . . . . . . . . . 12 (𝑁:𝑌1-1-onto→dom 𝑁𝑁 Fn 𝑌)
5754, 55, 563syl 18 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Fn 𝑌)
58 simprll 778 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑌)
59 simprr 772 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦)
6041adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋𝑌)
61 simprlr 779 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑋)
6260, 61sseldd 3946 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑌)
63 isorel 7272 . . . . . . . . . . . . . . 15 ((𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥𝑌𝑦𝑌)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6454, 58, 62, 63syl12anc 836 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6559, 64mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) E (𝑁𝑦))
66 fvex 6856 . . . . . . . . . . . . . 14 (𝑁𝑦) ∈ V
6766epeli 5540 . . . . . . . . . . . . 13 ((𝑁𝑥) E (𝑁𝑦) ↔ (𝑁𝑥) ∈ (𝑁𝑦))
6865, 67sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ (𝑁𝑦))
6922adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
7069cnveqd 5832 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
71 fnfun 6603 . . . . . . . . . . . . . . . . 17 (𝑁 Fn 𝑌 → Fun 𝑁)
72 funcnvres 6580 . . . . . . . . . . . . . . . . 17 (Fun 𝑁(𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7357, 71, 723syl 18 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7470, 73eqtrd 2777 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7574fveq1d 6845 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦))
7626adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
7761, 76eleqtrd 2840 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
7877fvresd 6863 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
7975, 78eqtrd 2777 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = (𝑁𝑦))
80 isocnv 7276 . . . . . . . . . . . . . . . . 17 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
8112, 80syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
82 isof1o 7269 . . . . . . . . . . . . . . . 16 (𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → 𝑀:𝑋1-1-onto→dom 𝑀)
83 f1of 6785 . . . . . . . . . . . . . . . 16 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
8481, 82, 833syl 18 . . . . . . . . . . . . . . 15 (𝜑𝑀:𝑋⟶dom 𝑀)
8584adantr 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀:𝑋⟶dom 𝑀)
8685, 61ffvelcdmd 7037 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) ∈ dom 𝑀)
8779, 86eqeltrrd 2839 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑦) ∈ dom 𝑀)
8810oicl 9466 . . . . . . . . . . . . 13 Ord dom 𝑀
89 ordtr1 6361 . . . . . . . . . . . . 13 (Ord dom 𝑀 → (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀))
9088, 89ax-mp 5 . . . . . . . . . . . 12 (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀)
9168, 87, 90syl2anc 585 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ dom 𝑀)
9257, 58, 91elpreimad 7010 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
93 imacnvcnv 6159 . . . . . . . . . . 11 (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)
9476, 93eqtr4di 2795 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
9592, 94eleqtrrd 2841 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑋)
9695, 61jca 513 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑋𝑦𝑋))
9796ex 414 . . . . . . 7 (𝜑 → (((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦) → (𝑥𝑋𝑦𝑋)))
9851, 97biimtrid 241 . . . . . 6 (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥𝑋𝑦𝑋)))
9922adantr 482 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
10099cnveqd 5832 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
101100fveq1d 6845 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑥) = ((𝑁 ↾ dom 𝑀)‘𝑥))
102100fveq1d 6845 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑦) = ((𝑁 ↾ dom 𝑀)‘𝑦))
103101, 102breq12d 5119 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑀𝑥) E (𝑀𝑦) ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
104 isorel 7272 . . . . . . . . . 10 ((𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
10581, 104sylan 581 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
106 eqidd 2738 . . . . . . . . . . . . 13 (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀))
107 isores3 7281 . . . . . . . . . . . . 13 ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
10834, 21, 106, 107syl3anc 1372 . . . . . . . . . . . 12 (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
109 isocnv 7276 . . . . . . . . . . . 12 ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
110108, 109syl 17 . . . . . . . . . . 11 (𝜑(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
111110adantr 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
112 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
11326adantr 482 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑋 = (𝑁 “ dom 𝑀))
114112, 113eleqtrd 2840 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
115 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
116115, 113eleqtrd 2840 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
117 isorel 7272 . . . . . . . . . 10 (((𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
118111, 114, 116, 117syl12anc 836 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
119103, 105, 1183bitr4d 311 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥𝑆𝑦))
12041sselda 3945 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑌)
121120adantrr 716 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑌)
122121, 115jca 513 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑌𝑦𝑋))
123122biantrurd 534 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)))
124123, 51bitr4di 289 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
125119, 124bitrd 279 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
126125ex 414 . . . . . 6 (𝜑 → ((𝑥𝑋𝑦𝑋) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)))
12750, 98, 126pm5.21ndd 381 . . . . 5 (𝜑 → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
128 df-br 5107 . . . . 5 (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
129 df-br 5107 . . . . 5 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋)))
130127, 128, 1293bitr3g 313 . . . 4 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋))))
131130eqrelrdv2 5752 . . 3 (((Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13247, 131mpancom 687 . 2 (𝜑𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13341, 132jca 513 1 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3065  Vcvv 3446  [wsbc 3740  cin 3910  wss 3911  {csn 4587  cop 4593   class class class wbr 5106  {copab 5168   E cep 5537   We wwe 5588   × cxp 5632  ccnv 5633  dom cdm 5634  ran crn 5635  cres 5636  cima 5637  Rel wrel 5639  Ord word 6317  Fun wfun 6491   Fn wfn 6492  wf 6493  ontowfo 6495  1-1-ontowf1o 6496  cfv 6497   Isom wiso 6498  (class class class)co 7358  OrdIsocoi 9446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-oi 9447
This theorem is referenced by:  fpwwe2lem9  10576
  Copyright terms: Public domain W3C validator