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 𝑋 ∧ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ ( ◡ 𝑅 “ { 𝑦 } ) ) = 𝑦 ) ) ) )