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

Theorem fpwwe 9725
Description: Given any function 𝐹 from the powerset of 𝐴 to 𝐴, canth2 8324 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 9108. 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 6849 . . . . . 6 (𝑌(𝐹 ∘ 1st )𝑅) = ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩)
2 fo1st 7390 . . . . . . . 8 1st :V–onto→V
3 fofn 6302 . . . . . . . 8 (1st :V–onto→V → 1st Fn V)
42, 3ax-mp 5 . . . . . . 7 1st Fn V
5 opex 5090 . . . . . . 7 𝑌, 𝑅⟩ ∈ V
6 fvco2 6466 . . . . . . 7 ((1st Fn V ∧ ⟨𝑌, 𝑅⟩ ∈ V) → ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩)))
74, 5, 6mp2an 683 . . . . . 6 ((𝐹 ∘ 1st )‘⟨𝑌, 𝑅⟩) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩))
81, 7eqtri 2787 . . . . 5 (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹‘(1st ‘⟨𝑌, 𝑅⟩))
9 fpwwe.1 . . . . . . . 8 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
109bropaex12 5364 . . . . . . 7 (𝑌𝑊𝑅 → (𝑌 ∈ V ∧ 𝑅 ∈ V))
11 op1stg 7382 . . . . . . 7 ((𝑌 ∈ V ∧ 𝑅 ∈ V) → (1st ‘⟨𝑌, 𝑅⟩) = 𝑌)
1210, 11syl 17 . . . . . 6 (𝑌𝑊𝑅 → (1st ‘⟨𝑌, 𝑅⟩) = 𝑌)
1312fveq2d 6383 . . . . 5 (𝑌𝑊𝑅 → (𝐹‘(1st ‘⟨𝑌, 𝑅⟩)) = (𝐹𝑌))
148, 13syl5eq 2811 . . . 4 (𝑌𝑊𝑅 → (𝑌(𝐹 ∘ 1st )𝑅) = (𝐹𝑌))
1514eleq1d 2829 . . 3 (𝑌𝑊𝑅 → ((𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌 ↔ (𝐹𝑌) ∈ 𝑌))
1615pm5.32i 570 . 2 ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌𝑊𝑅 ∧ (𝐹𝑌) ∈ 𝑌))
17 vex 3353 . . . . . . . . . . 11 𝑟 ∈ V
1817cnvex 7315 . . . . . . . . . 10 𝑟 ∈ V
1918imaex 7306 . . . . . . . . 9 (𝑟 “ {𝑦}) ∈ V
20 vex 3353 . . . . . . . . . . . 12 𝑢 ∈ V
2117inex1 4962 . . . . . . . . . . . 12 (𝑟 ∩ (𝑢 × 𝑢)) ∈ V
2220, 21algrflem 7492 . . . . . . . . . . 11 (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹𝑢)
23 fveq2 6379 . . . . . . . . . . 11 (𝑢 = (𝑟 “ {𝑦}) → (𝐹𝑢) = (𝐹‘(𝑟 “ {𝑦})))
2422, 23syl5eq 2811 . . . . . . . . . 10 (𝑢 = (𝑟 “ {𝑦}) → (𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = (𝐹‘(𝑟 “ {𝑦})))
2524eqeq1d 2767 . . . . . . . . 9 (𝑢 = (𝑟 “ {𝑦}) → ((𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(𝑟 “ {𝑦})) = 𝑦))
2619, 25sbcie 3633 . . . . . . . 8 ([(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ (𝐹‘(𝑟 “ {𝑦})) = 𝑦)
2726ralbii 3127 . . . . . . 7 (∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦 ↔ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦)
2827anbi2i 616 . . . . . 6 ((𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦) ↔ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))
2928anbi2i 616 . . . . 5 (((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦)) ↔ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦)))
3029opabbii 4878 . . . 4 {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))} = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐹‘(𝑟 “ {𝑦})) = 𝑦))}
319, 30eqtr4i 2790 . . 3 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 [(𝑟 “ {𝑦}) / 𝑢](𝑢(𝐹 ∘ 1st )(𝑟 ∩ (𝑢 × 𝑢))) = 𝑦))}
32 fpwwe.2 . . 3 (𝜑𝐴 ∈ V)
33 vex 3353 . . . . 5 𝑥 ∈ V
3433, 17algrflem 7492 . . . 4 (𝑥(𝐹 ∘ 1st )𝑟) = (𝐹𝑥)
35 simp1 1166 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥𝐴)
36 selpw 4324 . . . . . . 7 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
3735, 36sylibr 225 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
38 19.8a 2214 . . . . . . . 8 (𝑟 We 𝑥 → ∃𝑟 𝑟 We 𝑥)
39383ad2ant3 1165 . . . . . . 7 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → ∃𝑟 𝑟 We 𝑥)
40 ween 9113 . . . . . . 7 (𝑥 ∈ dom card ↔ ∃𝑟 𝑟 We 𝑥)
4139, 40sylibr 225 . . . . . 6 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ dom card)
4237, 41elind 3962 . . . . 5 ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ (𝒫 𝐴 ∩ dom card))
43 fpwwe.3 . . . . 5 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐹𝑥) ∈ 𝐴)
4442, 43sylan2 586 . . . 4 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝐹𝑥) ∈ 𝐴)
4534, 44syl5eqel 2848 . . 3 ((𝜑 ∧ (𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)) → (𝑥(𝐹 ∘ 1st )𝑟) ∈ 𝐴)
46 fpwwe.4 . . 3 𝑋 = dom 𝑊
4731, 32, 45, 46fpwwe2 9722 . 2 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝑌(𝐹 ∘ 1st )𝑅) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
4816, 47syl5bbr 276 1 (𝜑 → ((𝑌𝑊𝑅 ∧ (𝐹𝑌) ∈ 𝑌) ↔ (𝑌 = 𝑋𝑅 = (𝑊𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wral 3055  Vcvv 3350  [wsbc 3598  cin 3733  wss 3734  𝒫 cpw 4317  {csn 4336  cop 4342   cuni 4596   class class class wbr 4811  {copab 4873   We wwe 5237   × cxp 5277  ccnv 5278  dom cdm 5279  cima 5282  ccom 5283   Fn wfn 6065  ontowfo 6068  cfv 6070  (class class class)co 6846  1st c1st 7368  cardccrd 9016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7151
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6807  df-ov 6849  df-1st 7370  df-wrecs 7614  df-recs 7676  df-en 8165  df-oi 8626  df-card 9020
This theorem is referenced by:  canth4  9726  canthnumlem  9727  canthp1lem2  9732
  Copyright terms: Public domain W3C validator