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)

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

Proof

Step	Hyp	Ref	Expression
1		fpwwe.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
2		fpwwe.2	⊢ ( 𝜑 → 𝐴 ∈ V )
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	syl5eq	⊢ ( 𝑌 𝑊 𝑅 → ( 𝑌 ( 𝐹 ∘ 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	syl5eq	⊢ ( 𝑢 = ( ◡ 𝑟 “ { 𝑦 } ) → ( 𝑢 ( 𝐹 ∘ 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	syl5bbr	⊢ ( 𝜑 → ( ( 𝑌 𝑊 𝑅 ∧ ( 𝐹 ‘ 𝑌 ) ∈ 𝑌 ) ↔ ( 𝑌 = 𝑋 ∧ 𝑅 = ( 𝑊 ‘ 𝑋 ) ) ) )