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

Metamath Proof Explorer

Theorem fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024) (Proof shortened by Matthew House, 10-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝐴 ∈ 𝑉 )
5 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝑋 ⊆ 𝐴 )
6 4 5 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝑋 ∈ V )
7 6 6 xpexd ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ V )
8 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝑅 ⊆ ( 𝑋 × 𝑋 ) )
9 7 8 ssexd ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝑅 ∈ V )
10 simpl ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → 𝑥 = 𝑋 )
11 10 sseq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
12 simpr ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
13 10 sqxpeqd ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑥 × 𝑥 ) = ( 𝑋 × 𝑋 ) )
14 12 13 sseq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) )
15 12 10 weeq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑟 We 𝑥 ↔ 𝑅 We 𝑋 ) )
16 11 14 15 3anbi123d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) )
17 oveq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑥 𝐹 𝑟 ) = ( 𝑋 𝐹 𝑅 ) )
18 17 eleq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ↔ ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) )
19 16 18 imbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) ) )
20 3 ex ⊢ ( 𝜑 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) )
21 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) )
22 6 9 19 21 vtocl2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) )
23 22 syldbl2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 )