Theorem fpwwe2cbv

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 3-Jun-2015)

	Ref	Expression
Hypothesis	fpwwe2.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
Assertion	fpwwe2cbv	⊢ 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	⊢ 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) }
2		simpl	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → 𝑥 = 𝑎 )
3	2	sseq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑥 ⊆ 𝐴 ↔ 𝑎 ⊆ 𝐴 ) )
4		simpr	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → 𝑟 = 𝑠 )
5	2	sqxpeqd	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑥 × 𝑥 ) = ( 𝑎 × 𝑎 ) )
6	4 5	sseq12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 ⊆ ( 𝑥 × 𝑥 ) ↔ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) )
7	3 6	anbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ↔ ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ) )
8		weeq2	⊢ ( 𝑥 = 𝑎 → ( 𝑟 We 𝑥 ↔ 𝑟 We 𝑎 ) )
9		weeq1	⊢ ( 𝑟 = 𝑠 → ( 𝑟 We 𝑎 ↔ 𝑠 We 𝑎 ) )
10	8 9	sylan9bb	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 We 𝑥 ↔ 𝑠 We 𝑎 ) )
11		id	⊢ ( 𝑢 = 𝑣 → 𝑢 = 𝑣 )
12	11	sqxpeqd	⊢ ( 𝑢 = 𝑣 → ( 𝑢 × 𝑢 ) = ( 𝑣 × 𝑣 ) )
13	12	ineq2d	⊢ ( 𝑢 = 𝑣 → ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) = ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) )
14	11 13	oveq12d	⊢ ( 𝑢 = 𝑣 → ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) )
15	14	eqeq1d	⊢ ( 𝑢 = 𝑣 → ( ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ) )
16	15	cbvsbcvw	⊢ ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 )
17		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
18	17	imaeq2d	⊢ ( 𝑦 = 𝑧 → ( ◡ 𝑟 “ { 𝑦 } ) = ( ◡ 𝑟 “ { 𝑧 } ) )
19		eqeq2	⊢ ( 𝑦 = 𝑧 → ( ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ↔ ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
20	18 19	sbceqbid	⊢ ( 𝑦 = 𝑧 → ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
21	16 20	syl5bb	⊢ ( 𝑦 = 𝑧 → ( [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
22	21	cbvralvw	⊢ ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑧 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 )
23	4	cnveqd	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ◡ 𝑟 = ◡ 𝑠 )
24	23	imaeq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ◡ 𝑟 “ { 𝑧 } ) = ( ◡ 𝑠 “ { 𝑧 } ) )
25	4	ineq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) = ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) )
26	25	oveq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) )
27	26	eqeq1d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
28	24 27	sbceqbid	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
29	2 28	raleqbidv	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ∀ 𝑧 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑟 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ↔ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
30	22 29	syl5bb	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ↔ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) )
31	10 30	anbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ↔ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) )
32	7 31	anbi12d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑟 = 𝑠 ) → ( ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) ↔ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) ) )
33	32	cbvopabv	⊢ { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 [ ( ◡ 𝑟 “ { 𝑦 } ) / 𝑢 ] ( 𝑢 𝐹 ( 𝑟 ∩ ( 𝑢 × 𝑢 ) ) ) = 𝑦 ) ) } = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }
34	1 33	eqtri	⊢ 𝑊 = { ⟨ 𝑎 , 𝑠 ⟩ ∣ ( ( 𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ ( 𝑎 × 𝑎 ) ) ∧ ( 𝑠 We 𝑎 ∧ ∀ 𝑧 ∈ 𝑎 [ ( ◡ 𝑠 “ { 𝑧 } ) / 𝑣 ] ( 𝑣 𝐹 ( 𝑠 ∩ ( 𝑣 × 𝑣 ) ) ) = 𝑧 ) ) }