Metamath Proof Explorer

Theorem fpwwe2lem5

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

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

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.2 ⊢ ( 𝜑 → 𝐴 ∈ V )
3 fpwwe2.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 )
4 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → 𝐴 ∈ V )
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 6 9 jca ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) )
11 sseq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
12 xpeq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑥 = 𝑋 ) → ( 𝑥 × 𝑥 ) = ( 𝑋 × 𝑋 ) )
13 12 anidms ⊢ ( 𝑥 = 𝑋 → ( 𝑥 × 𝑥 ) = ( 𝑋 × 𝑋 ) )
14 13 sseq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ) )
15 weeq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑋 ) )
16 11 14 15 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ) )
17 16 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ) ) )
18 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐹 𝑟 ) = ( 𝑋 𝐹 𝑟 ) )
19 18 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ↔ ( 𝑋 𝐹 𝑟 ) ∈ 𝐴 ) )
20 17 19 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) ) → ( 𝑥 𝐹 𝑟 ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ) → ( 𝑋 𝐹 𝑟 ) ∈ 𝐴 ) ) )
21 sseq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ⊆ ( 𝑋 × 𝑋 ) ↔ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) )
22 weeq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 We 𝑋 ↔ 𝑅 We 𝑋 ) )
23 21 22 3anbi23d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ↔ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) )
24 23 anbi2d ⊢ ( 𝑟 = 𝑅 → ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) ) )
25 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑋 𝐹 𝑟 ) = ( 𝑋 𝐹 𝑅 ) )
26 25 eleq1d ⊢ ( 𝑟 = 𝑅 → ( ( 𝑋 𝐹 𝑟 ) ∈ 𝐴 ↔ ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) )
27 24 26 imbi12d ⊢ ( 𝑟 = 𝑅 → ( ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑟 We 𝑋 ) ) → ( 𝑋 𝐹 𝑟 ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) ) )
28 20 27 3 vtocl2g ⊢ ( ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) → ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 ) )
29 10 28 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ∧ 𝑅 We 𝑋 ) ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 )