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

Theorem fpwwe2lem8 10574
Description: Lemma for fpwwe2 10579. 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 5776 . . . . . . . . . 10 Rel 𝑊
43brrelex1i 5688 . . . . . . . . 9 (𝑋𝑊𝑅𝑋 ∈ V)
51, 4syl 17 . . . . . . . 8 (𝜑𝑋 ∈ V)
6 fpwwe2.2 . . . . . . . . . . 11 (𝜑𝐴𝑉)
72, 6fpwwe2lem2 10568 . . . . . . . . . 10 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
81, 7mpbid 231 . . . . . . . . 9 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
98simprld 770 . . . . . . . 8 (𝜑𝑅 We 𝑋)
10 fpwwe2lem8.m . . . . . . . . 9 𝑀 = OrdIso(𝑅, 𝑋)
1110oiiso 9473 . . . . . . . 8 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
125, 9, 11syl2anc 584 . . . . . . 7 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
13 isof1o 7268 . . . . . . 7 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
1412, 13syl 17 . . . . . 6 (𝜑𝑀:dom 𝑀1-1-onto𝑋)
15 f1ofo 6791 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋𝑀:dom 𝑀onto𝑋)
16 forn 6759 . . . . . 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 10573 . . . . . 6 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
2322rneqd 5893 . . . . 5 (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀))
2417, 23eqtr3d 2778 . . . 4 (𝜑𝑋 = ran (𝑁 ↾ dom 𝑀))
25 df-ima 5646 . . . 4 (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀)
2624, 25eqtr4di 2794 . . 3 (𝜑𝑋 = (𝑁 “ dom 𝑀))
27 imassrn 6024 . . . 4 (𝑁 “ dom 𝑀) ⊆ ran 𝑁
283brrelex1i 5688 . . . . . . . 8 (𝑌𝑊𝑆𝑌 ∈ V)
2919, 28syl 17 . . . . . . 7 (𝜑𝑌 ∈ V)
302, 6fpwwe2lem2 10568 . . . . . . . . 9 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
3119, 30mpbid 231 . . . . . . . 8 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
3231simprld 770 . . . . . . 7 (𝜑𝑆 We 𝑌)
3320oiiso 9473 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
3429, 32, 33syl2anc 584 . . . . . 6 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
35 isof1o 7268 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
3634, 35syl 17 . . . . 5 (𝜑𝑁:dom 𝑁1-1-onto𝑌)
37 f1ofo 6791 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
38 forn 6759 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
3936, 37, 383syl 18 . . . 4 (𝜑 → ran 𝑁 = 𝑌)
4027, 39sseqtrid 3996 . . 3 (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌)
4126, 40eqsstrd 3982 . 2 (𝜑𝑋𝑌)
428simplrd 768 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
43 relxp 5651 . . . . 5 Rel (𝑋 × 𝑋)
44 relss 5737 . . . . 5 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
4542, 43, 44mpisyl 21 . . . 4 (𝜑 → Rel 𝑅)
46 relinxp 5770 . . . 4 Rel (𝑆 ∩ (𝑌 × 𝑋))
4745, 46jctir 521 . . 3 (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))))
4842ssbrd 5148 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑥(𝑋 × 𝑋)𝑦))
49 brxp 5681 . . . . . . 7 (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥𝑋𝑦𝑋))
5048, 49syl6ib 250 . . . . . 6 (𝜑 → (𝑥𝑅𝑦 → (𝑥𝑋𝑦𝑋)))
51 brinxp2 5709 . . . . . . 7 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
52 isocnv 7275 . . . . . . . . . . . . . 14 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5334, 52syl 17 . . . . . . . . . . . . 13 (𝜑𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5453adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
55 isof1o 7268 . . . . . . . . . . . 12 (𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → 𝑁:𝑌1-1-onto→dom 𝑁)
56 f1ofn 6785 . . . . . . . . . . . 12 (𝑁:𝑌1-1-onto→dom 𝑁𝑁 Fn 𝑌)
5754, 55, 563syl 18 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Fn 𝑌)
58 simprll 777 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑌)
59 simprr 771 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦)
6041adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋𝑌)
61 simprlr 778 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑋)
6260, 61sseldd 3945 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑌)
63 isorel 7271 . . . . . . . . . . . . . . 15 ((𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥𝑌𝑦𝑌)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6454, 58, 62, 63syl12anc 835 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6559, 64mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) E (𝑁𝑦))
66 fvex 6855 . . . . . . . . . . . . . 14 (𝑁𝑦) ∈ V
6766epeli 5539 . . . . . . . . . . . . 13 ((𝑁𝑥) E (𝑁𝑦) ↔ (𝑁𝑥) ∈ (𝑁𝑦))
6865, 67sylib 217 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ (𝑁𝑦))
6922adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
7069cnveqd 5831 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
71 fnfun 6602 . . . . . . . . . . . . . . . . 17 (𝑁 Fn 𝑌 → Fun 𝑁)
72 funcnvres 6579 . . . . . . . . . . . . . . . . 17 (Fun 𝑁(𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7357, 71, 723syl 18 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7470, 73eqtrd 2776 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7574fveq1d 6844 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦))
7626adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
7761, 76eleqtrd 2840 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
7877fvresd 6862 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
7975, 78eqtrd 2776 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = (𝑁𝑦))
80 isocnv 7275 . . . . . . . . . . . . . . . . 17 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
8112, 80syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
82 isof1o 7268 . . . . . . . . . . . . . . . 16 (𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → 𝑀:𝑋1-1-onto→dom 𝑀)
83 f1of 6784 . . . . . . . . . . . . . . . 16 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
8481, 82, 833syl 18 . . . . . . . . . . . . . . 15 (𝜑𝑀:𝑋⟶dom 𝑀)
8584adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀:𝑋⟶dom 𝑀)
8685, 61ffvelcdmd 7036 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) ∈ dom 𝑀)
8779, 86eqeltrrd 2839 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑦) ∈ dom 𝑀)
8810oicl 9465 . . . . . . . . . . . . 13 Ord dom 𝑀
89 ordtr1 6360 . . . . . . . . . . . . 13 (Ord dom 𝑀 → (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀))
9088, 89ax-mp 5 . . . . . . . . . . . 12 (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀)
9168, 87, 90syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ dom 𝑀)
9257, 58, 91elpreimad 7009 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
93 imacnvcnv 6158 . . . . . . . . . . 11 (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)
9476, 93eqtr4di 2794 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
9592, 94eleqtrrd 2841 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑋)
9695, 61jca 512 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑋𝑦𝑋))
9796ex 413 . . . . . . 7 (𝜑 → (((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦) → (𝑥𝑋𝑦𝑋)))
9851, 97biimtrid 241 . . . . . 6 (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥𝑋𝑦𝑋)))
9922adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
10099cnveqd 5831 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
101100fveq1d 6844 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑥) = ((𝑁 ↾ dom 𝑀)‘𝑥))
102100fveq1d 6844 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑦) = ((𝑁 ↾ dom 𝑀)‘𝑦))
103101, 102breq12d 5118 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑀𝑥) E (𝑀𝑦) ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
104 isorel 7271 . . . . . . . . . 10 ((𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
10581, 104sylan 580 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
106 eqidd 2737 . . . . . . . . . . . . 13 (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀))
107 isores3 7280 . . . . . . . . . . . . 13 ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
10834, 21, 106, 107syl3anc 1371 . . . . . . . . . . . 12 (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
109 isocnv 7275 . . . . . . . . . . . 12 ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
110108, 109syl 17 . . . . . . . . . . 11 (𝜑(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
111110adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
112 simprl 769 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
11326adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑋 = (𝑁 “ dom 𝑀))
114112, 113eleqtrd 2840 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
115 simprr 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
116115, 113eleqtrd 2840 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
117 isorel 7271 . . . . . . . . . 10 (((𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
118111, 114, 116, 117syl12anc 835 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
119103, 105, 1183bitr4d 310 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥𝑆𝑦))
12041sselda 3944 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑌)
121120adantrr 715 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑌)
122121, 115jca 512 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑌𝑦𝑋))
123122biantrurd 533 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)))
124123, 51bitr4di 288 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
125119, 124bitrd 278 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
126125ex 413 . . . . . 6 (𝜑 → ((𝑥𝑋𝑦𝑋) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)))
12750, 98, 126pm5.21ndd 380 . . . . 5 (𝜑 → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
128 df-br 5106 . . . . 5 (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
129 df-br 5106 . . . . 5 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋)))
130127, 128, 1293bitr3g 312 . . . 4 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋))))
131130eqrelrdv2 5751 . . 3 (((Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13247, 131mpancom 686 . 2 (𝜑𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13341, 132jca 512 1 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  Vcvv 3445  [wsbc 3739  cin 3909  wss 3910  {csn 4586  cop 4592   class class class wbr 5105  {copab 5167   E cep 5536   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  Rel wrel 5638  Ord word 6316  Fun wfun 6490   Fn wfn 6491  wf 6492  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496   Isom wiso 6497  (class class class)co 7357  OrdIsocoi 9445
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-oi 9446
This theorem is referenced by:  fpwwe2lem9  10575
  Copyright terms: Public domain W3C validator