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

Metamath Proof Explorer

Theorem fpwwe2cbv

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 3-Jun-2015)

Ref Expression
Hypothesis fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
Assertion fpwwe2cbv 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → 𝑥 = 𝑎 )
3 2 sseq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
4 simpr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → 𝑟 = 𝑠 )
5 2 sqxpeqd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
6 4 5 sseq12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
7 3 6 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ) )
8 4 2 weeq12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 We 𝑥 ↔ 𝑠 We 𝑎 ) )
9 id ⊢ ( 𝑢 = 𝑣 → 𝑢 = 𝑣 )
10 9 sqxpeqd ⊢ ( 𝑢 = 𝑣 → ( 𝑢 × 𝑢 ) = ( 𝑣 × 𝑣 ) )
11 10 ineq2d ⊢ ( 𝑢 = 𝑣 → ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) )
12 9 11 oveq12d ⊢ ( 𝑢 = 𝑣 → ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) )
13 12 eqeq1d ⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ) )
14 13 cbvsbcvw ⊢ ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 )
15 sneq ⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
16 15 imaeq2d ⊢ ( 𝑦 = 𝑧 → ( ◡ 𝑟 “ { 𝑦 } ) = ( ◡ 𝑟 “ { 𝑧 } ) )
17 eqeq2 ⊢ ( 𝑦 = 𝑧 → ( ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ↔ ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
18 16 17 sbceqbid ⊢ ( 𝑦 = 𝑧 → ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
19 14 18 bitrid ⊢ ( 𝑦 = 𝑧 → ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
20 19 cbvralvw ⊢ ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑧 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 )
21 4 cnveqd ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ◡ 𝑟 = ◡ 𝑠 )
22 21 imaeq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ◡ 𝑟 “ { 𝑧 } ) = ( ◡ 𝑠 “ { 𝑧 } ) )
23 4 ineq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) = ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) )
24 23 oveq2d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) )
25 24 eqeq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
26 22 25 sbceqbid ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
27 2 26 raleqbidv ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ∀ 𝑧 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
28 20 27 bitrid ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
29 8 28 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ↔ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) )
30 7 29 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) ) )
31 30 cbvopabv ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }
32 1 31 eqtri ⊢ 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }