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

Theorem fpwwe2lem6 9401
Description: Lemma for fpwwe2 9409. (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 . . . . . . . 8 (𝜑𝑋𝑊𝑅)
2 fpwwe2.1 . . . . . . . . 9 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢𝐹(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
3 fpwwe2.2 . . . . . . . . 9 (𝜑𝐴 ∈ V)
42, 3fpwwe2lem2 9398 . . . . . . . 8 (𝜑 → (𝑋𝑊𝑅 ↔ ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))))
51, 4mpbid 222 . . . . . . 7 (𝜑 → ((𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)) ∧ (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦)))
65simpld 475 . . . . . 6 (𝜑 → (𝑋𝐴𝑅 ⊆ (𝑋 × 𝑋)))
76simprd 479 . . . . 5 (𝜑𝑅 ⊆ (𝑋 × 𝑋))
87ssbrd 4656 . . . 4 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶(𝑋 × 𝑋)(𝑀𝐵)))
9 brxp 5107 . . . . 5 (𝐶(𝑋 × 𝑋)(𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐵) ∈ 𝑋))
109simplbi 476 . . . 4 (𝐶(𝑋 × 𝑋)(𝑀𝐵) → 𝐶𝑋)
118, 10syl6 35 . . 3 (𝜑 → (𝐶𝑅(𝑀𝐵) → 𝐶𝑋))
1211imp 445 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑋)
13 imassrn 5436 . . . 4 (𝑁𝐵) ⊆ ran 𝑁
14 fpwwe2lem9.y . . . . . . . . 9 (𝜑𝑌𝑊𝑆)
152relopabi 5205 . . . . . . . . . 10 Rel 𝑊
1615brrelexi 5118 . . . . . . . . 9 (𝑌𝑊𝑆𝑌 ∈ V)
1714, 16syl 17 . . . . . . . 8 (𝜑𝑌 ∈ V)
182, 3fpwwe2lem2 9398 . . . . . . . . . . 11 (𝜑 → (𝑌𝑊𝑆 ↔ ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))))
1914, 18mpbid 222 . . . . . . . . . 10 (𝜑 → ((𝑌𝐴𝑆 ⊆ (𝑌 × 𝑌)) ∧ (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦)))
2019simprd 479 . . . . . . . . 9 (𝜑 → (𝑆 We 𝑌 ∧ ∀𝑦𝑌 [(𝑆 “ {𝑦}) / 𝑢](𝑢𝐹(𝑆 ∩ (𝑢 × 𝑢))) = 𝑦))
2120simpld 475 . . . . . . . 8 (𝜑𝑆 We 𝑌)
22 fpwwe2lem9.n . . . . . . . . 9 𝑁 = OrdIso(𝑆, 𝑌)
2322oiiso 8386 . . . . . . . 8 ((𝑌 ∈ V ∧ 𝑆 We 𝑌) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2417, 21, 23syl2anc 692 . . . . . . 7 (𝜑𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
2524adantr 481 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌))
26 isof1o 6527 . . . . . 6 (𝑁 Isom E , 𝑆 (dom 𝑁, 𝑌) → 𝑁:dom 𝑁1-1-onto𝑌)
2725, 26syl 17 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑁:dom 𝑁1-1-onto𝑌)
28 f1ofo 6101 . . . . 5 (𝑁:dom 𝑁1-1-onto𝑌𝑁:dom 𝑁onto𝑌)
29 forn 6075 . . . . 5 (𝑁:dom 𝑁onto𝑌 → ran 𝑁 = 𝑌)
3027, 28, 293syl 18 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → ran 𝑁 = 𝑌)
3113, 30syl5sseq 3632 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) ⊆ 𝑌)
3215brrelexi 5118 . . . . . . . . . . . . . 14 (𝑋𝑊𝑅𝑋 ∈ V)
331, 32syl 17 . . . . . . . . . . . . 13 (𝜑𝑋 ∈ V)
345simprd 479 . . . . . . . . . . . . . 14 (𝜑 → (𝑅 We 𝑋 ∧ ∀𝑦𝑋 [(𝑅 “ {𝑦}) / 𝑢](𝑢𝐹(𝑅 ∩ (𝑢 × 𝑢))) = 𝑦))
3534simpld 475 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝑋)
36 fpwwe2lem9.m . . . . . . . . . . . . . 14 𝑀 = OrdIso(𝑅, 𝑋)
3736oiiso 8386 . . . . . . . . . . . . 13 ((𝑋 ∈ V ∧ 𝑅 We 𝑋) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3833, 35, 37syl2anc 692 . . . . . . . . . . . 12 (𝜑𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
3938adantr 481 . . . . . . . . . . 11 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋))
40 isof1o 6527 . . . . . . . . . . 11 (𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) → 𝑀:dom 𝑀1-1-onto𝑋)
4139, 40syl 17 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:dom 𝑀1-1-onto𝑋)
42 f1ocnvfv2 6487 . . . . . . . . . 10 ((𝑀:dom 𝑀1-1-onto𝑋𝐶𝑋) → (𝑀‘(𝑀𝐶)) = 𝐶)
4341, 12, 42syl2anc 692 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶)) = 𝐶)
44 simpr 477 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑅(𝑀𝐵))
4543, 44eqbrtrd 4635 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵))
46 f1ocnv 6106 . . . . . . . . . . 11 (𝑀:dom 𝑀1-1-onto𝑋𝑀:𝑋1-1-onto→dom 𝑀)
47 f1of 6094 . . . . . . . . . . 11 (𝑀:𝑋1-1-onto→dom 𝑀𝑀:𝑋⟶dom 𝑀)
4841, 46, 473syl 18 . . . . . . . . . 10 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝑀:𝑋⟶dom 𝑀)
4948, 12ffvelrnd 6316 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ dom 𝑀)
50 fpwwe2lem7.1 . . . . . . . . . 10 (𝜑𝐵 ∈ dom 𝑀)
5150adantr 481 . . . . . . . . 9 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐵 ∈ dom 𝑀)
52 isorel 6530 . . . . . . . . 9 ((𝑀 Isom E , 𝑅 (dom 𝑀, 𝑋) ∧ ((𝑀𝐶) ∈ dom 𝑀𝐵 ∈ dom 𝑀)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5339, 49, 51, 52syl12anc 1321 . . . . . . . 8 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀‘(𝑀𝐶))𝑅(𝑀𝐵)))
5445, 53mpbird 247 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) E 𝐵)
55 epelg 4986 . . . . . . . 8 (𝐵 ∈ dom 𝑀 → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5651, 55syl 17 . . . . . . 7 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀𝐶) E 𝐵 ↔ (𝑀𝐶) ∈ 𝐵))
5754, 56mpbid 222 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) ∈ 𝐵)
58 ffn 6002 . . . . . . 7 (𝑀:𝑋⟶dom 𝑀𝑀 Fn 𝑋)
59 elpreima 6293 . . . . . . 7 (𝑀 Fn 𝑋 → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
6048, 58, 593syl 18 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶 ∈ (𝑀𝐵) ↔ (𝐶𝑋 ∧ (𝑀𝐶) ∈ 𝐵)))
6112, 57, 60mpbir2and 956 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
62 imacnvcnv 5558 . . . . 5 (𝑀𝐵) = (𝑀𝐵)
6361, 62syl6eleq 2708 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑀𝐵))
64 fpwwe2lem7.3 . . . . . . 7 (𝜑 → (𝑀𝐵) = (𝑁𝐵))
6564adantr 481 . . . . . 6 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
6665rneqd 5313 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → ran (𝑀𝐵) = ran (𝑁𝐵))
67 df-ima 5087 . . . . 5 (𝑀𝐵) = ran (𝑀𝐵)
68 df-ima 5087 . . . . 5 (𝑁𝐵) = ran (𝑁𝐵)
6966, 67, 683eqtr4g 2680 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
7063, 69eleqtrd 2700 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶 ∈ (𝑁𝐵))
7131, 70sseldd 3584 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → 𝐶𝑌)
7265cnveqd 5258 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑁𝐵))
73 dff1o3 6100 . . . . . . 7 (𝑀:dom 𝑀1-1-onto𝑋 ↔ (𝑀:dom 𝑀onto𝑋 ∧ Fun 𝑀))
7473simprbi 480 . . . . . 6 (𝑀:dom 𝑀1-1-onto𝑋 → Fun 𝑀)
75 funcnvres 5925 . . . . . 6 (Fun 𝑀(𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
7641, 74, 753syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐵) = (𝑀 ↾ (𝑀𝐵)))
77 dff1o3 6100 . . . . . . 7 (𝑁:dom 𝑁1-1-onto𝑌 ↔ (𝑁:dom 𝑁onto𝑌 ∧ Fun 𝑁))
7877simprbi 480 . . . . . 6 (𝑁:dom 𝑁1-1-onto𝑌 → Fun 𝑁)
79 funcnvres 5925 . . . . . 6 (Fun 𝑁(𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
8027, 78, 793syl 18 . . . . 5 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑁𝐵) = (𝑁 ↾ (𝑁𝐵)))
8172, 76, 803eqtr3d 2663 . . . 4 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀 ↾ (𝑀𝐵)) = (𝑁 ↾ (𝑁𝐵)))
8281fveq1d 6150 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = ((𝑁 ↾ (𝑁𝐵))‘𝐶))
83 fvres 6164 . . . 4 (𝐶 ∈ (𝑀𝐵) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
8463, 83syl 17 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑀 ↾ (𝑀𝐵))‘𝐶) = (𝑀𝐶))
85 fvres 6164 . . . 4 (𝐶 ∈ (𝑁𝐵) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8670, 85syl 17 . . 3 ((𝜑𝐶𝑅(𝑀𝐵)) → ((𝑁 ↾ (𝑁𝐵))‘𝐶) = (𝑁𝐶))
8782, 84, 863eqtr3d 2663 . 2 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝑀𝐶) = (𝑁𝐶))
8812, 71, 873jca 1240 1 ((𝜑𝐶𝑅(𝑀𝐵)) → (𝐶𝑋𝐶𝑌 ∧ (𝑀𝐶) = (𝑁𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  Vcvv 3186  [wsbc 3417  cin 3554  wss 3555  {csn 4148   class class class wbr 4613  {copab 4672   E cep 4983   We wwe 5032   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  Fun wfun 5841   Fn wfn 5842  wf 5843  ontowfo 5845  1-1-ontowf1o 5846  cfv 5847   Isom wiso 5848  (class class class)co 6604  OrdIsocoi 8358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-wrecs 7352  df-recs 7413  df-oi 8359
This theorem is referenced by:  fpwwe2lem7  9402
  Copyright terms: Public domain W3C validator