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

Theorem fpwwe2lem8 10676
Description: Lemma for fpwwe2 10681. 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 . . . . . . . 8 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . . . 10 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
32relopabiv 5833 . . . . . . . . 9 Rel 𝑊
43brrelex1i 5745 . . . . . . . 8 (𝑋𝑊𝑅𝑋 ∈ V)
51, 4syl 17 . . . . . . 7 (𝜑𝑋 ∈ V)
6 fpwwe2.2 . . . . . . . . . 10 (𝜑𝐴𝑉)
72, 6fpwwe2lem2 10670 . . . . . . . . 9 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
81, 7mpbid 232 . . . . . . . 8 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
98simprld 772 . . . . . . 7 (𝜑𝑅 We 𝑋)
10 fpwwe2lem8.m . . . . . . . 8 𝑀 = OrdIso(𝑅, 𝑋)
1110oiiso 9575 . . . . . . 7 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
125, 9, 11syl2anc 584 . . . . . 6 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
13 isof1o 7343 . . . . . 6 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
14 f1ofo 6856 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋𝑀:dom 𝑀onto𝑋)
15 forn 6824 . . . . . 6 (𝑀:dom 𝑀onto𝑋 → ran 𝑀 = 𝑋)
1612, 13, 14, 154syl 19 . . . . 5 (𝜑 → ran 𝑀 = 𝑋)
17 fpwwe2.3 . . . . . . 7 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
18 fpwwe2lem8.y . . . . . . 7 (𝜑𝑌𝑊𝑆)
19 fpwwe2lem8.n . . . . . . 7 𝑁 = OrdIso(𝑆, 𝑌)
20 fpwwe2lem8.s . . . . . . 7 (𝜑 → dom 𝑀 ⊆ dom 𝑁)
212, 6, 17, 1, 18, 10, 19, 20fpwwe2lem7 10675 . . . . . 6 (𝜑𝑀 = (𝑁 ↾ dom 𝑀))
2221rneqd 5952 . . . . 5 (𝜑 → ran 𝑀 = ran (𝑁 ↾ dom 𝑀))
2316, 22eqtr3d 2777 . . . 4 (𝜑𝑋 = ran (𝑁 ↾ dom 𝑀))
24 df-ima 5702 . . . 4 (𝑁 “ dom 𝑀) = ran (𝑁 ↾ dom 𝑀)
2523, 24eqtr4di 2793 . . 3 (𝜑𝑋 = (𝑁 “ dom 𝑀))
26 imassrn 6091 . . . 4 (𝑁 “ dom 𝑀) ⊆ ran 𝑁
273brrelex1i 5745 . . . . . . 7 (𝑌𝑊𝑆𝑌 ∈ V)
2818, 27syl 17 . . . . . 6 (𝜑𝑌 ∈ V)
292, 6fpwwe2lem2 10670 . . . . . . . 8 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
3018, 29mpbid 232 . . . . . . 7 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
3130simprld 772 . . . . . 6 (𝜑𝑆 We 𝑌)
3219oiiso 9575 . . . . . 6 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
3328, 31, 32syl2anc 584 . . . . 5 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
34 isof1o 7343 . . . . 5 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
35 f1ofo 6856 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
36 forn 6824 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
3733, 34, 35, 364syl 19 . . . 4 (𝜑 → ran 𝑁 = 𝑌)
3826, 37sseqtrid 4048 . . 3 (𝜑 → (𝑁 “ dom 𝑀) ⊆ 𝑌)
3925, 38eqsstrd 4034 . 2 (𝜑𝑋𝑌)
408simplrd 770 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
41 relxp 5707 . . . . 5 Rel (𝑋 × 𝑋)
42 relss 5794 . . . . 5 (𝑅 ⊆ (𝑋 × 𝑋) → (Rel (𝑋 × 𝑋) → Rel 𝑅))
4340, 41, 42mpisyl 21 . . . 4 (𝜑 → Rel 𝑅)
44 relinxp 5827 . . . 4 Rel (𝑆 ∩ (𝑌 × 𝑋))
4543, 44jctir 520 . . 3 (𝜑 → (Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))))
4640ssbrd 5191 . . . . . . 7 (𝜑 → (𝑥𝑅𝑦𝑥(𝑋 × 𝑋)𝑦))
47 brxp 5738 . . . . . . 7 (𝑥(𝑋 × 𝑋)𝑦 ↔ (𝑥𝑋𝑦𝑋))
4846, 47imbitrdi 251 . . . . . 6 (𝜑 → (𝑥𝑅𝑦 → (𝑥𝑋𝑦𝑋)))
49 brinxp2 5766 . . . . . . 7 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦))
50 isocnv 7350 . . . . . . . . . . . . . 14 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5133, 50syl 17 . . . . . . . . . . . . 13 (𝜑𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
5251adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Isom 𝑆, E (𝑌, dom 𝑁))
53 isof1o 7343 . . . . . . . . . . . 12 (𝑁 Isom 𝑆, E (𝑌, dom 𝑁) → 𝑁:𝑌1-1-onto→dom 𝑁)
54 f1ofn 6850 . . . . . . . . . . . 12 (𝑁:𝑌1-1-onto→dom 𝑁𝑁 Fn 𝑌)
5552, 53, 543syl 18 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑁 Fn 𝑌)
56 simprll 779 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑌)
57 simprr 773 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑆𝑦)
5839adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋𝑌)
59 simprlr 780 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑋)
6058, 59sseldd 3996 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦𝑌)
61 isorel 7346 . . . . . . . . . . . . . . 15 ((𝑁 Isom 𝑆, E (𝑌, dom 𝑁) ∧ (𝑥𝑌𝑦𝑌)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6252, 56, 60, 61syl12anc 837 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑆𝑦 ↔ (𝑁𝑥) E (𝑁𝑦)))
6357, 62mpbid 232 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) E (𝑁𝑦))
64 fvex 6920 . . . . . . . . . . . . . 14 (𝑁𝑦) ∈ V
6564epeli 5591 . . . . . . . . . . . . 13 ((𝑁𝑥) E (𝑁𝑦) ↔ (𝑁𝑥) ∈ (𝑁𝑦))
6663, 65sylib 218 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ (𝑁𝑦))
6721adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
6867cnveqd 5889 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ dom 𝑀))
69 fnfun 6669 . . . . . . . . . . . . . . . . 17 (𝑁 Fn 𝑌 → Fun 𝑁)
70 funcnvres 6646 . . . . . . . . . . . . . . . . 17 (Fun 𝑁(𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7155, 69, 703syl 18 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁 ↾ dom 𝑀) = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7268, 71eqtrd 2775 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀 = (𝑁 ↾ (𝑁 “ dom 𝑀)))
7372fveq1d 6909 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦))
7425adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
7559, 74eleqtrd 2841 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
7675fvresd 6927 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → ((𝑁 ↾ (𝑁 “ dom 𝑀))‘𝑦) = (𝑁𝑦))
7773, 76eqtrd 2775 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) = (𝑁𝑦))
78 isocnv 7350 . . . . . . . . . . . . . . . 16 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
79 isof1o 7343 . . . . . . . . . . . . . . . 16 (𝑀 Isom 𝑅, E (𝑋, dom 𝑀) → 𝑀:𝑋1-1-onto→dom 𝑀)
80 f1of 6849 . . . . . . . . . . . . . . . 16 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
8112, 78, 79, 804syl 19 . . . . . . . . . . . . . . 15 (𝜑𝑀:𝑋⟶dom 𝑀)
8281adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑀:𝑋⟶dom 𝑀)
8382, 59ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑀𝑦) ∈ dom 𝑀)
8477, 83eqeltrrd 2840 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑦) ∈ dom 𝑀)
8510oicl 9567 . . . . . . . . . . . . 13 Ord dom 𝑀
86 ordtr1 6429 . . . . . . . . . . . . 13 (Ord dom 𝑀 → (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀))
8785, 86ax-mp 5 . . . . . . . . . . . 12 (((𝑁𝑥) ∈ (𝑁𝑦) ∧ (𝑁𝑦) ∈ dom 𝑀) → (𝑁𝑥) ∈ dom 𝑀)
8866, 84, 87syl2anc 584 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑁𝑥) ∈ dom 𝑀)
8955, 56, 88elpreimad 7079 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
90 imacnvcnv 6228 . . . . . . . . . . 11 (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)
9174, 90eqtr4di 2793 . . . . . . . . . 10 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑋 = (𝑁 “ dom 𝑀))
9289, 91eleqtrrd 2842 . . . . . . . . 9 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → 𝑥𝑋)
9392, 59jca 511 . . . . . . . 8 ((𝜑 ∧ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)) → (𝑥𝑋𝑦𝑋))
9493ex 412 . . . . . . 7 (𝜑 → (((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦) → (𝑥𝑋𝑦𝑋)))
9549, 94biimtrid 242 . . . . . 6 (𝜑 → (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 → (𝑥𝑋𝑦𝑋)))
9621adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
9796cnveqd 5889 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑀 = (𝑁 ↾ dom 𝑀))
9897fveq1d 6909 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑥) = ((𝑁 ↾ dom 𝑀)‘𝑥))
9997fveq1d 6909 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑀𝑦) = ((𝑁 ↾ dom 𝑀)‘𝑦))
10098, 99breq12d 5161 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → ((𝑀𝑥) E (𝑀𝑦) ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
10112, 78syl 17 . . . . . . . . . 10 (𝜑𝑀 Isom 𝑅, E (𝑋, dom 𝑀))
102 isorel 7346 . . . . . . . . . 10 ((𝑀 Isom 𝑅, E (𝑋, dom 𝑀) ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
103101, 102sylan 580 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦 ↔ (𝑀𝑥) E (𝑀𝑦)))
104 eqidd 2736 . . . . . . . . . . . . 13 (𝜑 → (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀))
105 isores3 7355 . . . . . . . . . . . . 13 ((𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) ∧ dom 𝑀 ⊆ dom 𝑁 ∧ (𝑁 “ dom 𝑀) = (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
10633, 20, 104, 105syl3anc 1370 . . . . . . . . . . . 12 (𝜑 → (𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)))
107 isocnv 7350 . . . . . . . . . . . 12 ((𝑁 ↾ dom 𝑀) Isom E , 𝑆 (dom 𝑀, (𝑁 “ dom 𝑀)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
108106, 107syl 17 . . . . . . . . . . 11 (𝜑(𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
109108adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀))
110 simprl 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑋)
11125adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑋 = (𝑁 “ dom 𝑀))
112110, 111eleqtrd 2841 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥 ∈ (𝑁 “ dom 𝑀))
113 simprr 773 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦𝑋)
114113, 111eleqtrd 2841 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑦 ∈ (𝑁 “ dom 𝑀))
115 isorel 7346 . . . . . . . . . 10 (((𝑁 ↾ dom 𝑀) Isom 𝑆, E ((𝑁 “ dom 𝑀), dom 𝑀) ∧ (𝑥 ∈ (𝑁 “ dom 𝑀) ∧ 𝑦 ∈ (𝑁 “ dom 𝑀))) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
116109, 112, 114, 115syl12anc 837 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑁 ↾ dom 𝑀)‘𝑥) E ((𝑁 ↾ dom 𝑀)‘𝑦)))
117100, 103, 1163bitr4d 311 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥𝑆𝑦))
11839sselda 3995 . . . . . . . . . . . 12 ((𝜑𝑥𝑋) → 𝑥𝑌)
119118adantrr 717 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → 𝑥𝑌)
120119, 113jca 511 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑌𝑦𝑋))
121120biantrurd 532 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦 ↔ ((𝑥𝑌𝑦𝑋) ∧ 𝑥𝑆𝑦)))
122121, 49bitr4di 289 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑆𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
123117, 122bitrd 279 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦𝑋)) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
124123ex 412 . . . . . 6 (𝜑 → ((𝑥𝑋𝑦𝑋) → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦)))
12548, 95, 124pm5.21ndd 379 . . . . 5 (𝜑 → (𝑥𝑅𝑦𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦))
126 df-br 5149 . . . . 5 (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)
127 df-br 5149 . . . . 5 (𝑥(𝑆 ∩ (𝑌 × 𝑋))𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋)))
128125, 126, 1273bitr3g 313 . . . 4 (𝜑 → (⟨𝑥, 𝑦⟩ ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑆 ∩ (𝑌 × 𝑋))))
129128eqrelrdv2 5808 . . 3 (((Rel 𝑅 ∧ Rel (𝑆 ∩ (𝑌 × 𝑋))) ∧ 𝜑) → 𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13045, 129mpancom 688 . 2 (𝜑𝑅 = (𝑆 ∩ (𝑌 × 𝑋)))
13139, 130jca 511 1 (𝜑 → (𝑋𝑌𝑅 = (𝑆 ∩ (𝑌 × 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  Vcvv 3478  [wsbc 3791  cin 3962  wss 3963  {csn 4631  cop 4637   class class class wbr 5148  {copab 5210   E cep 5588   We wwe 5640   × cxp 5687  ccnv 5688  dom cdm 5689  ran crn 5690  cres 5691  cima 5692  Rel wrel 5694  Ord word 6385  Fun wfun 6557   Fn wfn 6558  wf 6559  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564  (class class class)co 7431  OrdIsocoi 9547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-oi 9548
This theorem is referenced by:  fpwwe2lem9  10677
  Copyright terms: Public domain W3C validator