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

Theorem fpwwe 9671
Description: Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 8270 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset 𝑋, (𝑊𝑋)⟩ which "agrees" with 𝐹 in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 9054. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
fpwwe.1 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
fpwwe.2 (𝜑𝐴 ∈ V)
fpwwe.3 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹𝑥) ∈ 𝐴)
fpwwe.4 𝑋 = dom 𝑊
Assertion
Ref Expression
fpwwe (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
Distinct variable groups:   𝑥,𝑟,𝐴   𝑦,𝑟,𝐹,𝑥   𝜑,𝑟,𝑥,𝑦   𝑅,𝑟,𝑥,𝑦   𝑋,𝑟,𝑥,𝑦   𝑌,𝑟,𝑥,𝑦   𝑊,𝑟,𝑥,𝑦
Allowed substitution hint:   𝐴(𝑦)

Proof of Theorem fpwwe
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 df-ov 6797 . . . . . 6 (𝑌(𝐹 ∘ 1st )𝑅) = ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩)
2 fo1st 7336 . . . . . . . 8 1st :V–onto→V
3 fofn 6259 . . . . . . . 8 (1st :V–onto→V → 1st Fn V)
42, 3ax-mp 5 . . . . . . 7 1st Fn V
5 opex 5061 . . . . . . 7 𝑌, 𝑅⟩ ∈ V
6 fvco2 6416 . . . . . . 7 ((1st Fn V ∧ ⟨𝑌, 𝑅⟩ ∈ V) → ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩)))
74, 5, 6mp2an 666 . . . . . 6 ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩))
81, 7eqtri 2793 . . . . 5 (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩))
9 fpwwe.1 . . . . . . . 8 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
109bropaex12 5333 . . . . . . 7 (𝑌𝑊𝑅 → (𝑌 ∈ V ∧ 𝑅 ∈ V))
11 op1stg 7328 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑅 ∈ V) → (1st ‘⟨𝑌, 𝑅⟩) = 𝑌)
1210, 11syl 17 . . . . . 6 (𝑌𝑊𝑅 → (1st ‘⟨𝑌, 𝑅⟩) = 𝑌)
1312fveq2d 6337 . . . . 5 (𝑌𝑊𝑅 → (𝐹‘(1st ‘⟨𝑌, 𝑅⟩)) = (𝐹𝑌))
148, 13syl5eq 2817 . . . 4 (𝑌𝑊𝑅 → (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹𝑌))
1514eleq1d 2835 . . 3 (𝑌𝑊𝑅 → ((𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌 ↔ (𝐹𝑌) ∈ 𝑌))
1615pm5.32i 558 . 2 ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌𝑊𝑅 ∧ (𝐹𝑌) ∈ 𝑌))
17 vex 3354 . . . . . . . . . . 11 𝑟 ∈ V
1817cnvex 7261 . . . . . . . . . 10 𝑟 ∈ V
1918imaex 7252 . . . . . . . . 9 (𝑟 “ {𝑦}) ∈ V
20 vex 3354 . . . . . . . . . . . 12 𝑢 ∈ V
2117inex1 4934 . . . . . . . . . . . 12 (𝑟 ∩ (𝑢 × 𝑢)) ∈ V
2220, 21algrflem 7438 . . . . . . . . . . 11 (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹𝑢)
23 fveq2 6333 . . . . . . . . . . 11 (𝑢 = (𝑟 “ {𝑦}) → (𝐹𝑢) = (𝐹‘(𝑟 “ {𝑦})))
2422, 23syl5eq 2817 . . . . . . . . . 10 (𝑢 = (𝑟 “ {𝑦}) → (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹‘(𝑟 “ {𝑦})))
2524eqeq1d 2773 . . . . . . . . 9 (𝑢 = (𝑟 “ {𝑦}) → ((𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(𝑟 “ {𝑦})) = 𝑦))
2619, 25sbcie 3623 . . . . . . . 8 ([(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(𝑟 “ {𝑦})) = 𝑦)
2726ralbii 3129 . . . . . . 7 (∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦)
2827anbi2i 603 . . . . . 6 ((𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))
2928anbi2i 603 . . . . 5 (((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦)))
3029opabbii 4852 . . . 4 {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
319, 30eqtr4i 2796 . . 3 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
32 fpwwe.2 . . 3 (𝜑𝐴 ∈ V)
33 vex 3354 . . . . 5 𝑥 ∈ V
3433, 17algrflem 7438 . . . 4 (𝑥(𝐹 ∘ 1st )𝑟) = (𝐹𝑥)
35 simp1 1130 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
36 selpw 4305 . . . . . . 7 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3735, 36sylibr 224 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
38 19.8a 2206 . . . . . . . 8 (𝑟 We 𝑥 → ∃𝑟 𝑟 We 𝑥)
39383ad2ant3 1129 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → ∃𝑟 𝑟 We 𝑥)
40 ween 9059 . . . . . . 7 (𝑥 ∈ dom card ↔ ∃𝑟 𝑟 We 𝑥)
4139, 40sylibr 224 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ dom card)
4237, 41elind 3950 . . . . 5 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ (𝒫 𝐴 ∩ dom card))
43 fpwwe.3 . . . . 5 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹𝑥) ∈ 𝐴)
4442, 43sylan2 574 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹𝑥) ∈ 𝐴)
4534, 44syl5eqel 2854 . . 3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥(𝐹 ∘ 1st )𝑟) ∈ 𝐴)
46 fpwwe.4 . . 3 𝑋 = dom 𝑊
4731, 32, 45, 46fpwwe2 9668 . 2 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
4816, 47syl5bbr 274 1 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wral 3061  Vcvv 3351  [wsbc 3588  cin 3723  wss 3724  𝒫 cpw 4298  {csn 4317  cop 4323   cuni 4575   class class class wbr 4787  {copab 4847   We wwe 5208   × cxp 5248  ccnv 5249  dom cdm 5250  cima 5253  ccom 5254   Fn wfn 6027  ontowfo 6030  cfv 6032  (class class class)co 6794  1st c1st 7314  cardccrd 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-isom 6041  df-riota 6755  df-ov 6797  df-1st 7316  df-wrecs 7560  df-recs 7622  df-en 8111  df-oi 8572  df-card 8966
This theorem is referenced by:  canth4  9672  canthnumlem  9673  canthp1lem2  9678
  Copyright terms: Public domain W3C validator