Theorem pr2pwpr

Description: The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018)

	Ref	Expression
Assertion	pr2pwpr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝑝 ∈ 𝒫 { 𝐴 , 𝐵 } ∣ 𝑝 ≈ 2o } = { { 𝐴 , 𝐵 } } )

Proof

Step	Hyp	Ref	Expression
1		elpwi	⊢ ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → 𝑠 ⊆ { 𝐴 , 𝐵 } )
2		prfi	⊢ { 𝐴 , 𝐵 } ∈ Fin
3		ssfi	⊢ ( ( { 𝐴 , 𝐵 } ∈ Fin ∧ 𝑠 ⊆ { 𝐴 , 𝐵 } ) → 𝑠 ∈ Fin )
4	2 3	mpan	⊢ ( 𝑠 ⊆ { 𝐴 , 𝐵 } → 𝑠 ∈ Fin )
5		hash2	⊢ ( ♯ ‘ 2o ) = 2
6	5	eqcomi	⊢ 2 = ( ♯ ‘ 2o )
7	6	a1i	⊢ ( 𝑠 ∈ Fin → 2 = ( ♯ ‘ 2o ) )
8	7	eqeq2d	⊢ ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) = 2 ↔ ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 2o ) ) )
9		2onn	⊢ 2o ∈ ω
10		nnfi	⊢ ( 2o ∈ ω → 2o ∈ Fin )
11	9 10	ax-mp	⊢ 2o ∈ Fin
12		hashen	⊢ ( ( 𝑠 ∈ Fin ∧ 2o ∈ Fin ) → ( ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 2o ) ↔ 𝑠 ≈ 2o ) )
13	11 12	mpan2	⊢ ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) = ( ♯ ‘ 2o ) ↔ 𝑠 ≈ 2o ) )
14	8 13	bitrd	⊢ ( 𝑠 ∈ Fin → ( ( ♯ ‘ 𝑠 ) = 2 ↔ 𝑠 ≈ 2o ) )
15		hash2pwpr	⊢ ( ( ( ♯ ‘ 𝑠 ) = 2 ∧ 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ) → 𝑠 = { 𝐴 , 𝐵 } )
16	15	a1d	⊢ ( ( ( ♯ ‘ 𝑠 ) = 2 ∧ 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) )
17	16	ex	⊢ ( ( ♯ ‘ 𝑠 ) = 2 → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) ) )
18	14 17	syl6bir	⊢ ( 𝑠 ∈ Fin → ( 𝑠 ≈ 2o → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) ) ) )
19	18	com23	⊢ ( 𝑠 ∈ Fin → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → ( 𝑠 ≈ 2o → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) ) ) )
20	4 19	syl	⊢ ( 𝑠 ⊆ { 𝐴 , 𝐵 } → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → ( 𝑠 ≈ 2o → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) ) ) )
21	1 20	mpcom	⊢ ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } → ( 𝑠 ≈ 2o → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) ) )
22	21	imp	⊢ ( ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → 𝑠 = { 𝐴 , 𝐵 } ) )
23	22	com12	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) → 𝑠 = { 𝐴 , 𝐵 } ) )
24		prex	⊢ { 𝐴 , 𝐵 } ∈ V
25	24	prid2	⊢ { 𝐴 , 𝐵 } ∈ { { 𝐵 } , { 𝐴 , 𝐵 } }
26	25	a1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } )
27	26	olcd	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ∈ { ∅ , { 𝐴 } } ∨ { 𝐴 , 𝐵 } ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
28		elun	⊢ ( { 𝐴 , 𝐵 } ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( { 𝐴 , 𝐵 } ∈ { ∅ , { 𝐴 } } ∨ { 𝐴 , 𝐵 } ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
29	27 28	sylibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
30		pwpr	⊢ 𝒫 { 𝐴 , 𝐵 } = ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } )
31	29 30	eleqtrrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝒫 { 𝐴 , 𝐵 } )
32	31	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → { 𝐴 , 𝐵 } ∈ 𝒫 { 𝐴 , 𝐵 } )
33		eleq1	⊢ ( 𝑠 = { 𝐴 , 𝐵 } → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } ∈ 𝒫 { 𝐴 , 𝐵 } ) )
34	33	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ↔ { 𝐴 , 𝐵 } ∈ 𝒫 { 𝐴 , 𝐵 } ) )
35	32 34	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } )
36		pr2nelem	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
37	36	adantr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → { 𝐴 , 𝐵 } ≈ 2o )
38		breq1	⊢ ( 𝑠 = { 𝐴 , 𝐵 } → ( 𝑠 ≈ 2o ↔ { 𝐴 , 𝐵 } ≈ 2o ) )
39	38	adantl	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → ( 𝑠 ≈ 2o ↔ { 𝐴 , 𝐵 } ≈ 2o ) )
40	37 39	mpbird	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → 𝑠 ≈ 2o )
41	35 40	jca	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑠 = { 𝐴 , 𝐵 } ) → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) )
42	41	ex	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑠 = { 𝐴 , 𝐵 } → ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) ) )
43	23 42	impbid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) ↔ 𝑠 = { 𝐴 , 𝐵 } ) )
44		breq1	⊢ ( 𝑝 = 𝑠 → ( 𝑝 ≈ 2o ↔ 𝑠 ≈ 2o ) )
45	44	elrab	⊢ ( 𝑠 ∈ { 𝑝 ∈ 𝒫 { 𝐴 , 𝐵 } ∣ 𝑝 ≈ 2o } ↔ ( 𝑠 ∈ 𝒫 { 𝐴 , 𝐵 } ∧ 𝑠 ≈ 2o ) )
46		velsn	⊢ ( 𝑠 ∈ { { 𝐴 , 𝐵 } } ↔ 𝑠 = { 𝐴 , 𝐵 } )
47	43 45 46	3bitr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑠 ∈ { 𝑝 ∈ 𝒫 { 𝐴 , 𝐵 } ∣ 𝑝 ≈ 2o } ↔ 𝑠 ∈ { { 𝐴 , 𝐵 } } ) )
48	47	eqrdv	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → { 𝑝 ∈ 𝒫 { 𝐴 , 𝐵 } ∣ 𝑝 ≈ 2o } = { { 𝐴 , 𝐵 } } )