Theorem sprsymrelfvlem

Description: Lemma for sprsymrelf and sprsymrelfv . (Contributed by AV, 19-Nov-2021)

	Ref	Expression
Assertion	sprsymrelfvlem	⊢ ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑉 ∈ V )
2		eleq1	⊢ ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐 ∈ 𝑃 ↔ { 𝑥 , 𝑦 } ∈ 𝑃 ) )
3		prsssprel	⊢ ( ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ∧ { 𝑥 , 𝑦 } ∈ 𝑃 ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
4	3	3exp	⊢ ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) )
5	4	com13	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) )
6	5	el2v	⊢ ( { 𝑥 , 𝑦 } ∈ 𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
7	2 6	biimtrdi	⊢ ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑐 ∈ 𝑃 → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) )
8	7	com12	⊢ ( 𝑐 ∈ 𝑃 → ( 𝑐 = { 𝑥 , 𝑦 } → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) )
9	8	rexlimiv	⊢ ( ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
10	9	com12	⊢ ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
11	10	adantl	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
12	11	imp	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
13	12	simpld	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → 𝑥 ∈ 𝑉 )
14	12	simprd	⊢ ( ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → 𝑦 ∈ 𝑉 )
15	1 1 13 14	opabex2	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ V )
16		elopab	⊢ ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) )
17	9	adantl	⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
18	17	adantld	⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
19	18	imp	⊢ ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
20		eleq1	⊢ ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
21	20	ad2antrr	⊢ ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ) )
22		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
23	21 22	bitrdi	⊢ ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → ( 𝑝 ∈ ( 𝑉 × 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
24	19 23	mpbird	⊢ ( ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) ∧ ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) )
25	24	ex	⊢ ( ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
26	25	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ) → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
27	16 26	sylbi	⊢ ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } → ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
28	27	com12	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → ( 𝑝 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } → 𝑝 ∈ ( 𝑉 × 𝑉 ) ) )
29	28	ssrdv	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ⊆ ( 𝑉 × 𝑉 ) )
30	15 29	elpwd	⊢ ( ( 𝑉 ∈ V ∧ 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
31	30	ex	⊢ ( 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ) )
32		fvprc	⊢ ( ¬ 𝑉 ∈ V → ( Pairs ‘ 𝑉 ) = ∅ )
33	32	sseq2d	⊢ ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑃 ⊆ ∅ ) )
34		ss0b	⊢ ( 𝑃 ⊆ ∅ ↔ 𝑃 = ∅ )
35	33 34	bitrdi	⊢ ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) ↔ 𝑃 = ∅ ) )
36		rex0	⊢ ¬ ∃ 𝑐 ∈ ∅ 𝑐 = { 𝑥 , 𝑦 }
37		rexeq	⊢ ( 𝑃 = ∅ → ( ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } ↔ ∃ 𝑐 ∈ ∅ 𝑐 = { 𝑥 , 𝑦 } ) )
38	36 37	mtbiri	⊢ ( 𝑃 = ∅ → ¬ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } )
39	38	alrimivv	⊢ ( 𝑃 = ∅ → ∀ 𝑥 ∀ 𝑦 ¬ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } )
40		opab0	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } = ∅ ↔ ∀ 𝑥 ∀ 𝑦 ¬ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } )
41	39 40	sylibr	⊢ ( 𝑃 = ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } = ∅ )
42		0elpw	⊢ ∅ ∈ 𝒫 ( 𝑉 × 𝑉 )
43	41 42	eqeltrdi	⊢ ( 𝑃 = ∅ → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )
44	35 43	biimtrdi	⊢ ( ¬ 𝑉 ∈ V → ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) ) )
45	31 44	pm2.61i	⊢ ( 𝑃 ⊆ ( Pairs ‘ 𝑉 ) → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑐 ∈ 𝑃 𝑐 = { 𝑥 , 𝑦 } } ∈ 𝒫 ( 𝑉 × 𝑉 ) )