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

Theorem fpwwe2lem6 10046
Description: Lemma for fpwwe2 10054. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe2.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
fpwwe2.2 (𝜑𝐴 ∈ V)
fpwwe2.3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥𝐹𝑟) ∈ 𝐴)
fpwwe2lem9.x (𝜑𝑋𝑊𝑅)
fpwwe2lem9.y (𝜑𝑌𝑊𝑆)
fpwwe2lem9.m 𝑀 = OrdIso(𝑅, 𝑋)
fpwwe2lem9.n 𝑁 = OrdIso(𝑆, 𝑌)
fpwwe2lem7.1 (𝜑𝐵 ∈ dom 𝑀)
fpwwe2lem7.2 (𝜑𝐵 ∈ dom 𝑁)
fpwwe2lem7.3 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
Assertion
Ref Expression
fpwwe2lem6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Distinct variable groups:   𝑦,𝑢,𝐵   𝑢,𝑟,𝑥,𝑦,𝐹   𝑋,𝑟,𝑢,𝑥,𝑦   𝑀,𝑟,𝑢,𝑥,𝑦   𝑁,𝑟,𝑢,𝑥,𝑦   𝜑,𝑟,𝑢,𝑥,𝑦   𝐴,𝑟,𝑥   𝑅,𝑟,𝑢,𝑥,𝑦   𝑌,𝑟,𝑢,𝑥,𝑦   𝑆,𝑟,𝑢,𝑥,𝑦   𝑊,𝑟,𝑢,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑦,𝑢)   𝐵(𝑥,𝑟)   𝐶(𝑥,𝑦,𝑢,𝑟)

Proof of Theorem fpwwe2lem6
StepHypRef Expression
1 fpwwe2lem9.x . . . . . . 7 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . 8 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . 8 (𝜑𝐴 ∈ V)
42, 3fpwwe2lem2 10043 . . . . . . 7 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
51, 4mpbid 235 . . . . . 6 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
65simplrd 769 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
76ssbrd 5073 . . . 4 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶(𝑋 × 𝑋)(𝑀𝐵)))
8 brxp 5565 . . . . 5 (𝐶(𝑋 × 𝑋)(𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐵) ∈ 𝑋))
98simplbi 501 . . . 4 (𝐶(𝑋 × 𝑋)(𝑀𝐵) → 𝐶𝑋)
107, 9syl6 35 . . 3 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶𝑋))
1110imp 410 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑋)
12 imassrn 5907 . . . 4 (𝑁𝐵) ⊆ ran 𝑁
13 fpwwe2lem9.y . . . . . . . . 9 (𝜑𝑌𝑊𝑆)
142relopabi 5658 . . . . . . . . . 10 Rel 𝑊
1514brrelex1i 5572 . . . . . . . . 9 (𝑌𝑊𝑆𝑌 ∈ V)
1613, 15syl 17 . . . . . . . 8 (𝜑𝑌 ∈ V)
172, 3fpwwe2lem2 10043 . . . . . . . . . 10 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
1813, 17mpbid 235 . . . . . . . . 9 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
1918simprld 771 . . . . . . . 8 (𝜑𝑆 We 𝑌)
20 fpwwe2lem9.n . . . . . . . . 9 𝑁 = OrdIso(𝑆, 𝑌)
2120oiiso 8985 . . . . . . . 8 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2216, 19, 21syl2anc 587 . . . . . . 7 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2322adantr 484 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
24 isof1o 7055 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
2523, 24syl 17 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁:dom 𝑁1-1-onto𝑌)
26 f1ofo 6597 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
27 forn 6568 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
2825, 26, 273syl 18 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → ran 𝑁 = 𝑌)
2912, 28sseqtrid 3967 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) ⊆ 𝑌)
3014brrelex1i 5572 . . . . . . . . . . . . . 14 (𝑋𝑊𝑅𝑋 ∈ V)
311, 30syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ V)
325simprld 771 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝑋)
33 fpwwe2lem9.m . . . . . . . . . . . . . 14 𝑀 = OrdIso(𝑅, 𝑋)
3433oiiso 8985 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3531, 32, 34syl2anc 587 . . . . . . . . . . . 12 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3635adantr 484 . . . . . . . . . . 11 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
37 isof1o 7055 . . . . . . . . . . 11 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
3836, 37syl 17 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:dom 𝑀1-1-onto𝑋)
39 f1ocnvfv2 7012 . . . . . . . . . 10 ((𝑀:dom 𝑀1-1-onto𝑋𝐶𝑋) → (𝑀‘(𝑀𝐶)) = 𝐶)
4038, 11, 39syl2anc 587 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶)) = 𝐶)
41 simpr 488 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑅(𝑀𝐵))
4240, 41eqbrtrd 5052 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵))
43 f1ocnv 6602 . . . . . . . . . . 11 (𝑀:dom 𝑀1-1-onto𝑋𝑀:𝑋1-1-onto→dom 𝑀)
44 f1of 6590 . . . . . . . . . . 11 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
4538, 43, 443syl 18 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:𝑋⟶dom 𝑀)
4645, 11ffvelrnd 6829 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ dom 𝑀)
47 fpwwe2lem7.1 . . . . . . . . . 10 (𝜑𝐵 ∈ dom 𝑀)
4847adantr 484 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐵 ∈ dom 𝑀)
49 isorel 7058 . . . . . . . . 9 ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((𝑀𝐶) ∈ dom 𝑀𝐵 ∈ dom 𝑀)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5036, 46, 48, 49syl12anc 835 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5142, 50mpbird 260 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) E 𝐵)
52 epelg 5431 . . . . . . . 8 (𝐵 ∈ dom 𝑀 → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5348, 52syl 17 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5451, 53mpbid 235 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ 𝐵)
55 ffn 6487 . . . . . . 7 (𝑀:𝑋⟶dom 𝑀𝑀 Fn 𝑋)
56 elpreima 6805 . . . . . . 7 (𝑀 Fn 𝑋 → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5745, 55, 563syl 18 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
5811, 54, 57mpbir2and 712 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
59 imacnvcnv 6030 . . . . 5 (𝑀𝐵) = (𝑀𝐵)
6058, 59eleqtrdi 2900 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
61 fpwwe2lem7.3 . . . . . . 7 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
6261adantr 484 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6362rneqd 5772 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → ran (𝑀𝐵) = ran (𝑁𝐵))
64 df-ima 5532 . . . . 5 (𝑀𝐵) = ran (𝑀𝐵)
65 df-ima 5532 . . . . 5 (𝑁𝐵) = ran (𝑁𝐵)
6663, 64, 653eqtr4g 2858 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6760, 66eleqtrd 2892 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑁𝐵))
6829, 67sseldd 3916 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑌)
6962cnveqd 5710 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
70 dff1o3 6596 . . . . . . 7 (𝑀:dom 𝑀1-1-onto𝑋 ↔ (𝑀:dom 𝑀onto𝑋 ∧ Fun 𝑀))
7170simprbi 500 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋 → Fun 𝑀)
72 funcnvres 6402 . . . . . 6 (Fun 𝑀(𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
7338, 71, 723syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
74 dff1o3 6596 . . . . . . 7 (𝑁:dom 𝑁1-1-onto𝑌 ↔ (𝑁:dom 𝑁onto𝑌 ∧ Fun 𝑁))
7574simprbi 500 . . . . . 6 (𝑁:dom 𝑁1-1-onto𝑌 → Fun 𝑁)
76 funcnvres 6402 . . . . . 6 (Fun 𝑁(𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7725, 75, 763syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
7869, 73, 773eqtr3d 2841 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀 ↾ (𝑀𝐵)) = (𝑁 ↾ (𝑁𝐵)))
7978fveq1d 6647 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = ((𝑁 ↾ (𝑁𝐵))‘𝐶))
8060fvresd 6665 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
8167fvresd 6665 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8279, 80, 813eqtr3d 2841 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) = (𝑁𝐶))
8311, 68, 823jca 1125 1 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2111  wral 3106  Vcvv 3441  [wsbc 3720  cin 3880  wss 3881  {csn 4525   class class class wbr 5030  {copab 5092   E cep 5429   We wwe 5477   × cxp 5517  ccnv 5518  dom cdm 5519  ran crn 5520  cres 5521  cima 5522  Fun wfun 6318   Fn wfn 6319  wf 6320  ontowfo 6322  1-1-ontowf1o 6323  cfv 6324   Isom wiso 6325  (class class class)co 7135  OrdIsocoi 8957
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-wrecs 7930  df-recs 7991  df-oi 8958
This theorem is referenced by:  fpwwe2lem7  10047
  Copyright terms: Public domain W3C validator