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

Theorem fpwwe2lem5 10658
Description: Lemma for fpwwe2 10666. (Contributed by Mario Carneiro, 18-May-2015.) (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(𝑆, 𝑌)
fpwwe2lem5.1 (𝜑𝐵 ∈ dom 𝑀)
fpwwe2lem5.2 (𝜑𝐵 ∈ dom 𝑁)
fpwwe2lem5.3 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
Assertion
Ref Expression
fpwwe2lem5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Distinct variable groups:   𝑦,𝑢,𝐵   𝑢,𝑟,𝑥,𝑦,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)   𝐵(𝑥,𝑟)   𝐶(𝑥,𝑦,𝑢,𝑟)   𝑉(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2lem5
StepHypRef Expression
1 fpwwe2lem8.x . . . . . . 7 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . 8 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . 8 (𝜑𝐴𝑉)
42, 3fpwwe2lem2 10655 . . . . . . 7 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
51, 4mpbid 231 . . . . . 6 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
65simplrd 768 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
76ssbrd 5186 . . . 4 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶(𝑋 × 𝑋)(𝑀𝐵)))
8 brxp 5721 . . . . 5 (𝐶(𝑋 × 𝑋)(𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐵) ∈ 𝑋))
98simplbi 496 . . . 4 (𝐶(𝑋 × 𝑋)(𝑀𝐵) → 𝐶𝑋)
107, 9syl6 35 . . 3 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶𝑋))
1110imp 405 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑋)
12 imassrn 6069 . . . 4 (𝑁𝐵) ⊆ ran 𝑁
13 fpwwe2lem8.y . . . . . . . . 9 (𝜑𝑌𝑊𝑆)
142relopabiv 5816 . . . . . . . . . 10 Rel 𝑊
1514brrelex1i 5728 . . . . . . . . 9 (𝑌𝑊𝑆𝑌 ∈ V)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ V)
172, 3fpwwe2lem2 10655 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
1813, 17mpbid 231 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
1918simprld 770 . . . . . . . 8 (𝜑𝑆 We 𝑌)
20 fpwwe2lem8.n . . . . . . . . 9 𝑁 = OrdIso(𝑆, 𝑌)
2120oiiso 9560 . . . . . . . 8 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2216, 19, 21syl2anc 582 . . . . . . 7 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2322adantr 479 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
24 isof1o 7327 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
2523, 24syl 17 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁:dom 𝑁1-1-onto𝑌)
26 f1ofo 6841 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
27 forn 6809 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
2825, 26, 273syl 18 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → ran 𝑁 = 𝑌)
2912, 28sseqtrid 4025 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) ⊆ 𝑌)
3014brrelex1i 5728 . . . . . . . . . . . . . 14 (𝑋𝑊𝑅𝑋 ∈ V)
311, 30syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ V)
325simprld 770 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝑋)
33 fpwwe2lem8.m . . . . . . . . . . . . . 14 𝑀 = OrdIso(𝑅, 𝑋)
3433oiiso 9560 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3531, 32, 34syl2anc 582 . . . . . . . . . . . 12 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3635adantr 479 . . . . . . . . . . 11 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37 isof1o 7327 . . . . . . . . . . 11 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
3836, 37syl 17 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:dom 𝑀1-1-onto𝑋)
39 f1ocnvfv2 7282 . . . . . . . . . 10 ((𝑀:dom 𝑀1-1-onto𝑋𝐶𝑋) → (𝑀‘(𝑀𝐶)) = 𝐶)
4038, 11, 39syl2anc 582 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶)) = 𝐶)
41 simpr 483 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑅(𝑀𝐵))
4240, 41eqbrtrd 5165 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵))
43 f1ocnv 6846 . . . . . . . . . . 11 (𝑀:dom 𝑀1-1-onto𝑋𝑀:𝑋1-1-onto→dom 𝑀)
44 f1of 6834 . . . . . . . . . . 11 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
4538, 43, 443syl 18 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:𝑋⟶dom 𝑀)
4645, 11ffvelcdmd 7090 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ dom 𝑀)
47 fpwwe2lem5.1 . . . . . . . . . 10 (𝜑𝐵 ∈ dom 𝑀)
4847adantr 479 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐵 ∈ dom 𝑀)
49 isorel 7330 . . . . . . . . 9 ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((𝑀𝐶) ∈ dom 𝑀𝐵 ∈ dom 𝑀)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5036, 46, 48, 49syl12anc 835 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5142, 50mpbird 256 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) E 𝐵)
52 epelg 5577 . . . . . . . 8 (𝐵 ∈ dom 𝑀 → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5348, 52syl 17 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5451, 53mpbid 231 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ 𝐵)
55 ffn 6717 . . . . . . 7 (𝑀:𝑋⟶dom 𝑀𝑀 Fn 𝑋)
56 elpreima 7062 . . . . . . 7 (𝑀 Fn 𝑋 → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5745, 55, 563syl 18 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5811, 54, 57mpbir2and 711 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
59 imacnvcnv 6205 . . . . 5 (𝑀𝐵) = (𝑀𝐵)
6058, 59eleqtrdi 2835 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
61 fpwwe2lem5.3 . . . . . . 7 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
6261adantr 479 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6362rneqd 5934 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → ran (𝑀𝐵) = ran (𝑁𝐵))
64 df-ima 5685 . . . . 5 (𝑀𝐵) = ran (𝑀𝐵)
65 df-ima 5685 . . . . 5 (𝑁𝐵) = ran (𝑁𝐵)
6663, 64, 653eqtr4g 2790 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6760, 66eleqtrd 2827 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑁𝐵))
6829, 67sseldd 3973 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑌)
6962cnveqd 5872 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
70 dff1o3 6840 . . . . . . 7 (𝑀:dom 𝑀1-1-onto𝑋 ↔ (𝑀:dom 𝑀onto𝑋 ∧ Fun 𝑀))
7170simprbi 495 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋 → Fun 𝑀)
72 funcnvres 6626 . . . . . 6 (Fun 𝑀(𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
7338, 71, 723syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
74 dff1o3 6840 . . . . . . 7 (𝑁:dom 𝑁1-1-onto𝑌 ↔ (𝑁:dom 𝑁onto𝑌 ∧ Fun 𝑁))
7574simprbi 495 . . . . . 6 (𝑁:dom 𝑁1-1-onto𝑌 → Fun 𝑁)
76 funcnvres 6626 . . . . . 6 (Fun 𝑁(𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7725, 75, 763syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7869, 73, 773eqtr3d 2773 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀 ↾ (𝑀𝐵)) = (𝑁 ↾ (𝑁𝐵)))
7978fveq1d 6894 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = ((𝑁 ↾ (𝑁𝐵))‘𝐶))
8060fvresd 6912 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
8167fvresd 6912 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8279, 80, 813eqtr3d 2773 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) = (𝑁𝐶))
8311, 68, 823jca 1125 1 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  wral 3051  Vcvv 3463  [wsbc 3768  cin 3938  wss 3939  {csn 4624   class class class wbr 5143  {copab 5205   E cep 5575   We wwe 5626   × cxp 5670  ccnv 5671  dom cdm 5672  ran crn 5673  cres 5674  cima 5675  Fun wfun 6537   Fn wfn 6538  wf 6539  ontowfo 6541  1-1-ontowf1o 6542  cfv 6543   Isom wiso 6544  (class class class)co 7416  OrdIsocoi 9532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7372  df-ov 7419  df-2nd 7992  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-oi 9533
This theorem is referenced by:  fpwwe2lem6  10659
  Copyright terms: Public domain W3C validator