Theorem fpwwe2lem3

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 19-May-2015) (Revised by AV, 20-Jul-2024)

	Ref	Expression
Hypotheses	fpwwe2.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
	fpwwe2.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	fpwwe2lem3.4	⊢ ( 𝜑 → 𝑋 𝑊 𝑅 )
Assertion	fpwwe2lem3	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2		fpwwe2.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		fpwwe2lem3.4	⊢ ( 𝜑 → 𝑋 𝑊 𝑅 )
4	1 2	fpwwe2lem2	⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
5	3 4	mpbid	⊢ ( 𝜑 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
6	5	simprrd	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 )
7		sneq	⊢ ( 𝑦 = 𝐵 → { 𝑦 } = { 𝐵 } )
8	7	imaeq2d	⊢ ( 𝑦 = 𝐵 → ( ◡ 𝑅 “ { 𝑦 } ) = ( ◡ 𝑅 “ { 𝐵 } ) )
9		eqeq2	⊢ ( 𝑦 = 𝐵 → ( ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ) )
10	8 9	sbceqbid	⊢ ( 𝑦 = 𝐵 → ( [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ) )
11	10	rspccva	⊢ ( ( ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ∧ 𝐵 ∈ 𝑋 ) → [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 )
12	6 11	sylan	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 )
13		cnvimass	⊢ ( ◡ 𝑅 “ { 𝐵 } ) ⊆ dom 𝑅
14	1	relopabiv	⊢ Rel 𝑊
15	14	brrelex2i	⊢ ( 𝑋 𝑊 𝑅 → 𝑅 ∈ V )
16		dmexg	⊢ ( 𝑅 ∈ V → dom 𝑅 ∈ V )
17	3 15 16	3syl	⊢ ( 𝜑 → dom 𝑅 ∈ V )
18		ssexg	⊢ ( ( ( ◡ 𝑅 “ { 𝐵 } ) ⊆ dom 𝑅 ∧ dom 𝑅 ∈ V ) → ( ◡ 𝑅 “ { 𝐵 } ) ∈ V )
19	13 17 18	sylancr	⊢ ( 𝜑 → ( ◡ 𝑅 “ { 𝐵 } ) ∈ V )
20		id	⊢ ( 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) → 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) )
21	20	sqxpeqd	⊢ ( 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) → ( 𝑢 × 𝑢 ) = ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) )
22	21	ineq2d	⊢ ( 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) → ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) )
23	20 22	oveq12d	⊢ ( 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) → ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) )
24	23	eqeq1d	⊢ ( 𝑢 = ( ◡ 𝑅 “ { 𝐵 } ) → ( ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ↔ ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 ) )
25	24	sbcieg	⊢ ( ( ◡ 𝑅 “ { 𝐵 } ) ∈ V → ( [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ↔ ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 ) )
26	19 25	syl	⊢ ( 𝜑 → ( [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ↔ ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( [ ( ◡ 𝑅 “ { 𝐵 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝐵 ↔ ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 ) )
28	12 27	mpbid	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 )