prproropreud

Description: There is exactly one ordered ordered pair fulfilling a wff iff there is exactly one proper pair fulfilling an equivalent wff. (Contributed by AV, 20-Mar-2023)

	Ref	Expression
Hypotheses	prproropreud.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
	prproropreud.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
	prproropreud.b	⊢ ( 𝜑 → 𝑅 Or 𝑉 )
	prproropreud.x	⊢ ( 𝑥 = ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ → ( 𝜓 ↔ 𝜒 ) )
	prproropreud.z	⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
Assertion	prproropreud	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝑂 𝜓 ↔ ∃! 𝑦 ∈ 𝑃 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		prproropreud.o	⊢ 𝑂 = ( 𝑅 ∩ ( 𝑉 × 𝑉 ) )
2		prproropreud.p	⊢ 𝑃 = { 𝑝 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑝 ) = 2 }
3		prproropreud.b	⊢ ( 𝜑 → 𝑅 Or 𝑉 )
4		prproropreud.x	⊢ ( 𝑥 = ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ → ( 𝜓 ↔ 𝜒 ) )
5		prproropreud.z	⊢ ( 𝑥 = 𝑧 → ( 𝜓 ↔ 𝜃 ) )
6		eqid	⊢ ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ )
7	1 2 6	prproropf1o	⊢ ( 𝑅 Or 𝑉 → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) : 𝑃 –1-1-onto→ 𝑂 )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) : 𝑃 –1-1-onto→ 𝑂 )
9		sbceq1a	⊢ ( 𝑥 = ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) → ( 𝜓 ↔ [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) ) → ( 𝜓 ↔ [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
11		nfsbc1v	⊢ Ⅎ 𝑥 [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓
12	8 10 5 11	reuf1odnf	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝑂 𝜓 ↔ ∃! 𝑦 ∈ 𝑃 [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ) )
13		eqidd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) = ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) )
14		infeq1	⊢ ( 𝑝 = 𝑦 → inf ( 𝑝 , 𝑉 , 𝑅 ) = inf ( 𝑦 , 𝑉 , 𝑅 ) )
15		supeq1	⊢ ( 𝑝 = 𝑦 → sup ( 𝑝 , 𝑉 , 𝑅 ) = sup ( 𝑦 , 𝑉 , 𝑅 ) )
16	14 15	opeq12d	⊢ ( 𝑝 = 𝑦 → ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ = ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ )
17	16	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑝 = 𝑦 ) → ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ = ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → 𝑦 ∈ 𝑃 )
19		opex	⊢ ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ ∈ V
20	19	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ ∈ V )
21	13 17 18 20	fvmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) = ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ )
22	21	sbceq1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ [ ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ / 𝑥 ] 𝜓 ) )
23	4	sbcieg	⊢ ( ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ ∈ V → ( [ ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ / 𝑥 ] 𝜓 ↔ 𝜒 ) )
24	20 23	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( [ ⟨ inf ( 𝑦 , 𝑉 , 𝑅 ) , sup ( 𝑦 , 𝑉 , 𝑅 ) ⟩ / 𝑥 ] 𝜓 ↔ 𝜒 ) )
25	22 24	bitrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ 𝜒 ) )
26	25	reubidva	⊢ ( 𝜑 → ( ∃! 𝑦 ∈ 𝑃 [ ( ( 𝑝 ∈ 𝑃 ↦ ⟨ inf ( 𝑝 , 𝑉 , 𝑅 ) , sup ( 𝑝 , 𝑉 , 𝑅 ) ⟩ ) ‘ 𝑦 ) / 𝑥 ] 𝜓 ↔ ∃! 𝑦 ∈ 𝑃 𝜒 ) )
27	12 26	bitrd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝑂 𝜓 ↔ ∃! 𝑦 ∈ 𝑃 𝜒 ) )

Metamath Proof Explorer

Theorem prproropreud

Proof