Metamath Proof Explorer

Theorem fpwwe2lem2

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

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

Proof

Step Hyp Ref Expression
1 fpwwe2.1 ⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2 fpwwe2.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 weeq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑋 ) )
21 weeq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 We 𝑋 ↔ 𝑅 We 𝑋 ) )
22 20 21 sylan9bb ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑟 We 𝑥 ↔ 𝑅 We 𝑋 ) )
23 16 cnveqd ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ◡ 𝑟 = ◡ 𝑅 )
24 23 imaeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ◡ 𝑟 “ { 𝑦 } ) = ( ◡ 𝑅 “ { 𝑦 } ) )
25 16 ineq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) )
26 25 oveq2d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) )
27 26 eqeq1d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
28 24 27 sbceqbid ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
29 14 28 raleqbidv ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) )
30 22 29 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ↔ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) )
31 19 30 anbi12d ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
32 31 1 brabga ⊢ ( ( 𝑋 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )
33 6 13 32 pm5.21nd ⊢ ( 𝜑 → ( 𝑋 𝑊 𝑅 ↔ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑅 ⊆ ( 𝑋 × 𝑋 ) ) ∧ ( 𝑅 We 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 [ ( ◡ 𝑅 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑅 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ) )