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

Theorem fpwwe2lem5 10391
Description: Lemma for fpwwe2 10399. (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 10388 . . . . . . 7 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
51, 4mpbid 231 . . . . . 6 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
65simplrd 767 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
76ssbrd 5117 . . . 4 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶(𝑋 × 𝑋)(𝑀𝐵)))
8 brxp 5636 . . . . 5 (𝐶(𝑋 × 𝑋)(𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐵) ∈ 𝑋))
98simplbi 498 . . . 4 (𝐶(𝑋 × 𝑋)(𝑀𝐵) → 𝐶𝑋)
107, 9syl6 35 . . 3 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶𝑋))
1110imp 407 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑋)
12 imassrn 5980 . . . 4 (𝑁𝐵) ⊆ ran 𝑁
13 fpwwe2lem8.y . . . . . . . . 9 (𝜑𝑌𝑊𝑆)
142relopabiv 5730 . . . . . . . . . 10 Rel 𝑊
1514brrelex1i 5643 . . . . . . . . 9 (𝑌𝑊𝑆𝑌 ∈ V)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ V)
172, 3fpwwe2lem2 10388 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
1813, 17mpbid 231 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
1918simprld 769 . . . . . . . 8 (𝜑𝑆 We 𝑌)
20 fpwwe2lem8.n . . . . . . . . 9 𝑁 = OrdIso(𝑆, 𝑌)
2120oiiso 9296 . . . . . . . 8 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2216, 19, 21syl2anc 584 . . . . . . 7 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2322adantr 481 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
24 isof1o 7194 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
2523, 24syl 17 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁:dom 𝑁1-1-onto𝑌)
26 f1ofo 6723 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
27 forn 6691 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
2825, 26, 273syl 18 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → ran 𝑁 = 𝑌)
2912, 28sseqtrid 3973 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) ⊆ 𝑌)
3014brrelex1i 5643 . . . . . . . . . . . . . 14 (𝑋𝑊𝑅𝑋 ∈ V)
311, 30syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ V)
325simprld 769 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝑋)
33 fpwwe2lem8.m . . . . . . . . . . . . . 14 𝑀 = OrdIso(𝑅, 𝑋)
3433oiiso 9296 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3531, 32, 34syl2anc 584 . . . . . . . . . . . 12 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3635adantr 481 . . . . . . . . . . 11 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37 isof1o 7194 . . . . . . . . . . 11 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
3836, 37syl 17 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:dom 𝑀1-1-onto𝑋)
39 f1ocnvfv2 7149 . . . . . . . . . 10 ((𝑀:dom 𝑀1-1-onto𝑋𝐶𝑋) → (𝑀‘(𝑀𝐶)) = 𝐶)
4038, 11, 39syl2anc 584 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶)) = 𝐶)
41 simpr 485 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑅(𝑀𝐵))
4240, 41eqbrtrd 5096 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵))
43 f1ocnv 6728 . . . . . . . . . . 11 (𝑀:dom 𝑀1-1-onto𝑋𝑀:𝑋1-1-onto→dom 𝑀)
44 f1of 6716 . . . . . . . . . . 11 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
4538, 43, 443syl 18 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:𝑋⟶dom 𝑀)
4645, 11ffvelrnd 6962 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ dom 𝑀)
47 fpwwe2lem5.1 . . . . . . . . . 10 (𝜑𝐵 ∈ dom 𝑀)
4847adantr 481 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐵 ∈ dom 𝑀)
49 isorel 7197 . . . . . . . . 9 ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((𝑀𝐶) ∈ dom 𝑀𝐵 ∈ dom 𝑀)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5036, 46, 48, 49syl12anc 834 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5142, 50mpbird 256 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) E 𝐵)
52 epelg 5496 . . . . . . . 8 (𝐵 ∈ dom 𝑀 → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5348, 52syl 17 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5451, 53mpbid 231 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ 𝐵)
55 ffn 6600 . . . . . . 7 (𝑀:𝑋⟶dom 𝑀𝑀 Fn 𝑋)
56 elpreima 6935 . . . . . . 7 (𝑀 Fn 𝑋 → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5745, 55, 563syl 18 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5811, 54, 57mpbir2and 710 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
59 imacnvcnv 6109 . . . . 5 (𝑀𝐵) = (𝑀𝐵)
6058, 59eleqtrdi 2849 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
61 fpwwe2lem5.3 . . . . . . 7 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
6261adantr 481 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6362rneqd 5847 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → ran (𝑀𝐵) = ran (𝑁𝐵))
64 df-ima 5602 . . . . 5 (𝑀𝐵) = ran (𝑀𝐵)
65 df-ima 5602 . . . . 5 (𝑁𝐵) = ran (𝑁𝐵)
6663, 64, 653eqtr4g 2803 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6760, 66eleqtrd 2841 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑁𝐵))
6829, 67sseldd 3922 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑌)
6962cnveqd 5784 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
70 dff1o3 6722 . . . . . . 7 (𝑀:dom 𝑀1-1-onto𝑋 ↔ (𝑀:dom 𝑀onto𝑋 ∧ Fun 𝑀))
7170simprbi 497 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋 → Fun 𝑀)
72 funcnvres 6512 . . . . . 6 (Fun 𝑀(𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
7338, 71, 723syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
74 dff1o3 6722 . . . . . . 7 (𝑁:dom 𝑁1-1-onto𝑌 ↔ (𝑁:dom 𝑁onto𝑌 ∧ Fun 𝑁))
7574simprbi 497 . . . . . 6 (𝑁:dom 𝑁1-1-onto𝑌 → Fun 𝑁)
76 funcnvres 6512 . . . . . 6 (Fun 𝑁(𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7725, 75, 763syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7869, 73, 773eqtr3d 2786 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀 ↾ (𝑀𝐵)) = (𝑁 ↾ (𝑁𝐵)))
7978fveq1d 6776 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = ((𝑁 ↾ (𝑁𝐵))‘𝐶))
8060fvresd 6794 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
8167fvresd 6794 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8279, 80, 813eqtr3d 2786 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) = (𝑁𝐶))
8311, 68, 823jca 1127 1 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wcel 2106  wral 3064  Vcvv 3432  [wsbc 3716  cin 3886  wss 3887  {csn 4561   class class class wbr 5074  {copab 5136   E cep 5494   We wwe 5543   × cxp 5587  ccnv 5588  dom cdm 5589  ran crn 5590  cres 5591  cima 5592  Fun wfun 6427   Fn wfn 6428  wf 6429  ontowfo 6431  1-1-ontowf1o 6432  cfv 6433   Isom wiso 6434  (class class class)co 7275  OrdIsocoi 9268
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-oi 9269
This theorem is referenced by:  fpwwe2lem6  10392
  Copyright terms: Public domain W3C validator