This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑋 ) → ( ( ◡ 𝑅 “ { 𝐵 } ) 𝐹 ( 𝑅 ∩ ( ( ◡ 𝑅 “ { 𝐵 } ) × ( ◡ 𝑅 “ { 𝐵 } ) ) ) ) = 𝐵 )