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

Theorem fpwwe2lem5 10626
Description: Lemma for fpwwe2 10634. (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 10623 . . . . . . 7 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
51, 4mpbid 231 . . . . . 6 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
65simplrd 767 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
76ssbrd 5181 . . . 4 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶(𝑋 × 𝑋)(𝑀𝐵)))
8 brxp 5715 . . . . 5 (𝐶(𝑋 × 𝑋)(𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐵) ∈ 𝑋))
98simplbi 497 . . . 4 (𝐶(𝑋 × 𝑋)(𝑀𝐵) → 𝐶𝑋)
107, 9syl6 35 . . 3 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶𝑋))
1110imp 406 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑋)
12 imassrn 6060 . . . 4 (𝑁𝐵) ⊆ ran 𝑁
13 fpwwe2lem8.y . . . . . . . . 9 (𝜑𝑌𝑊𝑆)
142relopabiv 5810 . . . . . . . . . 10 Rel 𝑊
1514brrelex1i 5722 . . . . . . . . 9 (𝑌𝑊𝑆𝑌 ∈ V)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ V)
172, 3fpwwe2lem2 10623 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
1813, 17mpbid 231 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
1918simprld 769 . . . . . . . 8 (𝜑𝑆 We 𝑌)
20 fpwwe2lem8.n . . . . . . . . 9 𝑁 = OrdIso(𝑆, 𝑌)
2120oiiso 9528 . . . . . . . 8 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2216, 19, 21syl2anc 583 . . . . . . 7 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2322adantr 480 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
24 isof1o 7312 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
2523, 24syl 17 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁:dom 𝑁1-1-onto𝑌)
26 f1ofo 6830 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
27 forn 6798 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
2825, 26, 273syl 18 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → ran 𝑁 = 𝑌)
2912, 28sseqtrid 4026 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) ⊆ 𝑌)
3014brrelex1i 5722 . . . . . . . . . . . . . 14 (𝑋𝑊𝑅𝑋 ∈ V)
311, 30syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ V)
325simprld 769 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝑋)
33 fpwwe2lem8.m . . . . . . . . . . . . . 14 𝑀 = OrdIso(𝑅, 𝑋)
3433oiiso 9528 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3531, 32, 34syl2anc 583 . . . . . . . . . . . 12 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3635adantr 480 . . . . . . . . . . 11 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37 isof1o 7312 . . . . . . . . . . 11 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
3836, 37syl 17 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:dom 𝑀1-1-onto𝑋)
39 f1ocnvfv2 7267 . . . . . . . . . 10 ((𝑀:dom 𝑀1-1-onto𝑋𝐶𝑋) → (𝑀‘(𝑀𝐶)) = 𝐶)
4038, 11, 39syl2anc 583 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶)) = 𝐶)
41 simpr 484 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑅(𝑀𝐵))
4240, 41eqbrtrd 5160 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵))
43 f1ocnv 6835 . . . . . . . . . . 11 (𝑀:dom 𝑀1-1-onto𝑋𝑀:𝑋1-1-onto→dom 𝑀)
44 f1of 6823 . . . . . . . . . . 11 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
4538, 43, 443syl 18 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:𝑋⟶dom 𝑀)
4645, 11ffvelcdmd 7077 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ dom 𝑀)
47 fpwwe2lem5.1 . . . . . . . . . 10 (𝜑𝐵 ∈ dom 𝑀)
4847adantr 480 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐵 ∈ dom 𝑀)
49 isorel 7315 . . . . . . . . 9 ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((𝑀𝐶) ∈ dom 𝑀𝐵 ∈ dom 𝑀)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5036, 46, 48, 49syl12anc 834 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5142, 50mpbird 257 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) E 𝐵)
52 epelg 5571 . . . . . . . 8 (𝐵 ∈ dom 𝑀 → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5348, 52syl 17 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5451, 53mpbid 231 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ 𝐵)
55 ffn 6707 . . . . . . 7 (𝑀:𝑋⟶dom 𝑀𝑀 Fn 𝑋)
56 elpreima 7049 . . . . . . 7 (𝑀 Fn 𝑋 → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5745, 55, 563syl 18 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5811, 54, 57mpbir2and 710 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
59 imacnvcnv 6195 . . . . 5 (𝑀𝐵) = (𝑀𝐵)
6058, 59eleqtrdi 2835 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
61 fpwwe2lem5.3 . . . . . . 7 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
6261adantr 480 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6362rneqd 5927 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → ran (𝑀𝐵) = ran (𝑁𝐵))
64 df-ima 5679 . . . . 5 (𝑀𝐵) = ran (𝑀𝐵)
65 df-ima 5679 . . . . 5 (𝑁𝐵) = ran (𝑁𝐵)
6663, 64, 653eqtr4g 2789 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6760, 66eleqtrd 2827 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑁𝐵))
6829, 67sseldd 3975 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑌)
6962cnveqd 5865 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
70 dff1o3 6829 . . . . . . 7 (𝑀:dom 𝑀1-1-onto𝑋 ↔ (𝑀:dom 𝑀onto𝑋 ∧ Fun 𝑀))
7170simprbi 496 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋 → Fun 𝑀)
72 funcnvres 6616 . . . . . 6 (Fun 𝑀(𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
7338, 71, 723syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
74 dff1o3 6829 . . . . . . 7 (𝑁:dom 𝑁1-1-onto𝑌 ↔ (𝑁:dom 𝑁onto𝑌 ∧ Fun 𝑁))
7574simprbi 496 . . . . . 6 (𝑁:dom 𝑁1-1-onto𝑌 → Fun 𝑁)
76 funcnvres 6616 . . . . . 6 (Fun 𝑁(𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7725, 75, 763syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7869, 73, 773eqtr3d 2772 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀 ↾ (𝑀𝐵)) = (𝑁 ↾ (𝑁𝐵)))
7978fveq1d 6883 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = ((𝑁 ↾ (𝑁𝐵))‘𝐶))
8060fvresd 6901 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
8167fvresd 6901 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8279, 80, 813eqtr3d 2772 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) = (𝑁𝐶))
8311, 68, 823jca 1125 1 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wral 3053  Vcvv 3466  [wsbc 3769  cin 3939  wss 3940  {csn 4620   class class class wbr 5138  {copab 5200   E cep 5569   We wwe 5620   × cxp 5664  ccnv 5665  dom cdm 5666  ran crn 5667  cres 5668  cima 5669  Fun wfun 6527   Fn wfn 6528  wf 6529  ontowfo 6531  1-1-ontowf1o 6532  cfv 6533   Isom wiso 6534  (class class class)co 7401  OrdIsocoi 9500
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 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-se 5622  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7357  df-ov 7404  df-2nd 7969  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-oi 9501
This theorem is referenced by:  fpwwe2lem6  10627
  Copyright terms: Public domain W3C validator