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

Metamath Proof Explorer

Theorem fpwwe2lem1

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015)

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

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 simpll ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑥 ⊆ 𝐴 )
3 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
4 2 3 sylibr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑥 ∈ 𝒫 𝐴 )
5 simplr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ⊆ ( 𝑥 × 𝑥 ) )
6 xpss12 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
7 2 2 6 syl2anc ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
8 5 7 sstrd ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
9 velpw ⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
10 8 9 sylibr ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
11 4 10 jca ⊢ ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) )
12 11 ssopab2i ⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } ⊆ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) }
13 df-xp ⊢ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) ) = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) }
14 12 1 13 3sstr4i ⊢ 𝑊 ⊆ ( 𝒫 𝐴 × 𝒫 ( 𝐴 × 𝐴 ) )