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

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 relopabiv ⊢ 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 16 14 weeq12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑟 We 𝑥 ↔ 𝑅 We 𝑋 ) )
21 16 cnveqd ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ◡ 𝑟 = ◡ 𝑅 )
22 21 imaeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ◡ 𝑟 “ { 𝑦 } ) = ( ◡ 𝑅 “ { 𝑦 } ) )
23 22 fveqeq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ↔ ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) )
24 14 23 raleqbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) )
25 20 24 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ↔ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) )
26 19 25 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐹 ‘ ( ◡ 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )
27 26 1 brabga ⊢ ( ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )
28 6 13 27 pm5.21nd ⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )