Metamath Proof Explorer


Theorem fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024)

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 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 𝑋 ) ) → ( 𝑋 𝐹 𝑅 ) ∈ 𝐴 )