Metamath Proof Explorer


Theorem fpwwe

Description: Given any function F from the powerset of A to A , canth2 gives that the function is not injective, but we can say rather more than that. There is a unique well-ordered subset <. X , ( WX ) >. which "agrees" with F 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 . Theorem 1.1 of KanamoriPincus p. 415. (Contributed by Mario Carneiro, 18-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
fpwwe.2 ( 𝜑𝐴𝑉 )
fpwwe.3 ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐹𝑥 ) ∈ 𝐴 )
fpwwe.4 𝑋 = dom 𝑊
Assertion fpwwe ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝐹𝑌 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋𝑅 = ( 𝑊𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 fpwwe.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
2 fpwwe.2 ( 𝜑𝐴𝑉 )
3 fpwwe.3 ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐹𝑥 ) ∈ 𝐴 )
4 fpwwe.4 𝑋 = dom 𝑊
5 df-ov ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝑌 , 𝑅 ⟩ )
6 fo1st 1st : V –onto→ V
7 fofn ( 1st : V –onto→ V → 1st Fn V )
8 6 7 ax-mp 1st Fn V
9 opex 𝑌 , 𝑅 ⟩ ∈ V
10 fvco2 ( ( 1st Fn V ∧ ⟨ 𝑌 , 𝑅 ⟩ ∈ V ) → ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝑌 , 𝑅 ⟩ ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) ) )
11 8 9 10 mp2an ( ( 𝐹 ∘ 1st ) ‘ ⟨ 𝑌 , 𝑅 ⟩ ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) )
12 5 11 eqtri ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) )
13 1 bropaex12 ( 𝑌 𝑊 𝑅 → ( 𝑌 ∈ V ∧ 𝑅 ∈ V ) )
14 op1stg ( ( 𝑌 ∈ V ∧ 𝑅 ∈ V ) → ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) = 𝑌 )
15 13 14 syl ( 𝑌 𝑊 𝑅 → ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) = 𝑌 )
16 15 fveq2d ( 𝑌 𝑊 𝑅 → ( 𝐹 ‘ ( 1st ‘ ⟨ 𝑌 , 𝑅 ⟩ ) ) = ( 𝐹𝑌 ) )
17 12 16 eqtrid ( 𝑌 𝑊 𝑅 → ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) = ( 𝐹𝑌 ) )
18 17 eleq1d ( 𝑌 𝑊 𝑅 → ( ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ↔ ( 𝐹𝑌 ) ∈ 𝑌 ) )
19 18 pm5.32i ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑌 𝑊 𝑅 ∧ ( 𝐹𝑌 ) ∈ 𝑌 ) )
20 vex 𝑟 ∈ V
21 20 cnvex 𝑟 ∈ V
22 21 imaex ( 𝑟 “ { 𝑦 } ) ∈ V
23 vex 𝑢 ∈ V
24 20 inex1 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ∈ V
25 23 24 algrflem ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝐹𝑢 )
26 fveq2 ( 𝑢 = ( 𝑟 “ { 𝑦 } ) → ( 𝐹𝑢 ) = ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) )
27 25 26 eqtrid ( 𝑢 = ( 𝑟 “ { 𝑦 } ) → ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) )
28 27 eqeq1d ( 𝑢 = ( 𝑟 “ { 𝑦 } ) → ( ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) )
29 22 28 sbcie ( [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 )
30 29 ralbii ( ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 )
31 30 anbi2i ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ↔ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) )
32 31 anbi2i ( ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ↔ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) )
33 32 opabbii { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
34 1 33 eqtr4i 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 [ ( 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 ( 𝐹 ∘ 1st ) ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
35 vex 𝑥 ∈ V
36 35 20 algrflem ( 𝑥 ( 𝐹 ∘ 1st ) 𝑟 ) = ( 𝐹𝑥 )
37 simp1 ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥𝐴 )
38 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
39 37 38 sylibr ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
40 19.8a ( 𝑟 We 𝑥 → ∃ 𝑟 𝑟 We 𝑥 )
41 40 3ad2ant3 ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ∃ 𝑟 𝑟 We 𝑥 )
42 ween ( 𝑥 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝑥 )
43 41 42 sylibr ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ dom card )
44 39 43 elind ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) )
45 44 3 sylan2 ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝐹𝑥 ) ∈ 𝐴 )
46 36 45 eqeltrid ( ( 𝜑 ∧ ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 ( 𝐹 ∘ 1st ) 𝑟 ) ∈ 𝐴 )
47 34 2 46 4 fpwwe2 ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝑌 ( 𝐹 ∘ 1st ) 𝑅 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋𝑅 = ( 𝑊𝑋 ) ) ) )
48 19 47 bitr3id ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝐹𝑌 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋𝑅 = ( 𝑊𝑋 ) ) ) )