# Metamath Proof Explorer

## Theorem fpwwelem

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

Ref Expression
Hypotheses fpwwe.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
fpwwe.2 ( 𝜑𝐴𝑉 )
Assertion fpwwelem ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )

### Proof

Step Hyp Ref Expression
1 fpwwe.1 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
2 fpwwe.2 ( 𝜑𝐴𝑉 )
3 1 relopabi Rel 𝑊
4 3 a1i ( 𝜑 → Rel 𝑊 )
5 brrelex12 ( ( Rel 𝑊𝑋 𝑊 𝑅 ) → ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) )
6 4 5 sylan ( ( 𝜑𝑋 𝑊 𝑅 ) → ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) )
7 2 adantr ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → 𝐴𝑉 )
8 simprll ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → 𝑋𝐴 )
9 7 8 ssexd ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → 𝑋 ∈ V )
10 9 9 xpexd ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → ( 𝑋 × 𝑋 ) ∈ V )
11 simprlr ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → 𝑅 ⊆ ( 𝑋 × 𝑋 ) )
12 10 11 ssexd ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → 𝑅 ∈ V )
13 9 12 jca ( ( 𝜑 ∧ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) → ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) )
14 simpl ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → 𝑥 = 𝑋 )
15 14 sseq1d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( 𝑥𝐴𝑋𝐴 ) )
16 simpr ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
17 14 sqxpeqd ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( 𝑥 × 𝑥 ) = ( 𝑋 × 𝑋 ) )
18 16 17 sseq12d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) )
19 15 18 anbi12d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ↔ ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ) )
20 weeq2 ( 𝑥 = 𝑋 → ( 𝑟 We 𝑥𝑟 We 𝑋 ) )
21 weeq1 ( 𝑟 = 𝑅 → ( 𝑟 We 𝑋𝑅 We 𝑋 ) )
22 20 21 sylan9bb ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( 𝑟 We 𝑥𝑅 We 𝑋 ) )
23 16 cnveqd ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
24 23 imaeq1d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( 𝑟 “ { 𝑦 } ) = ( 𝑅 “ { 𝑦 } ) )
25 24 fveqeq2d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ↔ ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) )
26 14 25 raleqbidv ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ↔ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) )
27 22 26 anbi12d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ↔ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) )
28 19 27 anbi12d ( ( 𝑥 = 𝑋𝑟 = 𝑅 ) → ( ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐹 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )
29 28 1 brabga ( ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )
30 6 13 29 pm5.21nd ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋𝐴𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦𝑋 ( 𝐹 ‘ ( 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )