Metamath Proof Explorer

Theorem paireqne

Description: Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023)

Ref Expression
Hypotheses paireqne.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
paireqne.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
paireqne.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion paireqne ( 𝜑 → ( ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ 𝐴 ≠ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 paireqne.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 paireqne.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 paireqne.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
4 raleq ⊢ ( 𝑝 = 𝑞 → ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
5 4 reu8 ⊢ ( ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∃ 𝑝 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) )
6 3 eleq2i ⊢ ( 𝑝 ∈ 𝑃 ↔ 𝑝 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 elss2prb ⊢ ( 𝑝 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) )
8 6 7 bitri ⊢ ( 𝑝 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) )
9 raleq ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∀ 𝑥 ∈ { 𝑎 , 𝑏 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
10 vex ⊢ 𝑎 ∈ V
11 vex ⊢ 𝑏 ∈ V
12 eqeq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 = 𝐴 ↔ 𝑎 = 𝐴 ) )
13 eqeq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 = 𝐵 ↔ 𝑎 = 𝐵 ) )
14 12 13 orbi12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) )
15 eqeq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 = 𝐴 ↔ 𝑏 = 𝐴 ) )
16 eqeq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 = 𝐵 ↔ 𝑏 = 𝐵 ) )
17 15 16 orbi12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) )
18 10 11 14 17 ralpr ⊢ ( ∀ 𝑥 ∈ { 𝑎 , 𝑏 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) )
19 9 18 bitrdi ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) )
20 eqeq1 ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( 𝑝 = 𝑞 ↔ { 𝑎 , 𝑏 } = 𝑞 ) )
21 20 imbi2d ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ↔ ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ) )
22 21 ralbidv ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ↔ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ) )
23 19 22 anbi12d ⊢ ( 𝑝 = { 𝑎 , 𝑏 } → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) ↔ ( ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ) ) )
24 23 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) ↔ ( ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ) ) )
25 1 2 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
26 prelpwi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
27 25 26 syl ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
28 27 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
29 hashprg ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
31 30 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 ≠ 𝑏 → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
32 31 com12 ⊢ ( 𝑎 ≠ 𝑏 → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
33 32 adantr ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
34 33 impcom ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
35 34 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
36 eqtr3 ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐴 ) → 𝑏 = 𝑎 )
37 eqneqall ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≠ 𝑏 → ( 𝑝 = { 𝑎 , 𝑏 } → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
38 37 impd ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
39 38 a1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
40 39 impd ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
41 40 equcoms ⊢ ( 𝑏 = 𝑎 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
42 36 41 syl ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐴 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
43 42 ex ⊢ ( 𝑏 = 𝐴 → ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
44 preq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
45 44 eqcomd ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
46 45 a1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
47 46 expcom ⊢ ( 𝑏 = 𝐵 → ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
48 43 47 jaoi ⊢ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( 𝑎 = 𝐴 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
49 48 com12 ⊢ ( 𝑎 = 𝐴 → ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
50 prcom ⊢ { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
51 preq12 ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐵 ) → { 𝑏 , 𝑎 } = { 𝐴 , 𝐵 } )
52 50 51 syl5eq ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
53 52 eqcomd ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐵 ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
54 53 a1d ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
55 54 ex ⊢ ( 𝑏 = 𝐴 → ( 𝑎 = 𝐵 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
56 eqtr3 ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐵 ) → 𝑏 = 𝑎 )
57 56 41 syl ⊢ ( ( 𝑏 = 𝐵 ∧ 𝑎 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
58 57 ex ⊢ ( 𝑏 = 𝐵 → ( 𝑎 = 𝐵 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
59 55 58 jaoi ⊢ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( 𝑎 = 𝐵 → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
60 59 com12 ⊢ ( 𝑎 = 𝐵 → ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
61 49 60 jaoi ⊢ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) ) )
62 61 imp ⊢ ( ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) → ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } ) )
63 62 impcom ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → { 𝐴 , 𝐵 } = { 𝑎 , 𝑏 } )
64 63 fveqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
65 35 64 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
66 28 65 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
67 3 eleq2i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝑃 ↔ { 𝐴 , 𝐵 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
68 fveqeq2 ⊢ ( 𝑥 = { 𝐴 , 𝐵 } → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
69 68 elrab ⊢ ( { 𝐴 , 𝐵 } ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
70 67 69 bitri ⊢ ( { 𝐴 , 𝐵 } ∈ 𝑃 ↔ ( { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
71 66 70 sylibr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → { 𝐴 , 𝐵 } ∈ 𝑃 )
72 raleq ⊢ ( 𝑞 = { 𝐴 , 𝐵 } → ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
73 eqeq2 ⊢ ( 𝑞 = { 𝐴 , 𝐵 } → ( { 𝑎 , 𝑏 } = 𝑞 ↔ { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
74 72 73 imbi12d ⊢ ( 𝑞 = { 𝐴 , 𝐵 } → ( ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ↔ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
75 74 rspcv ⊢ ( { 𝐴 , 𝐵 } ∈ 𝑃 → ( ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
76 71 75 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
77 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
78 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )
79 77 78 orbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ) )
80 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐴 ↔ 𝐵 = 𝐴 ) )
81 eqeq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 = 𝐵 ↔ 𝐵 = 𝐵 ) )
82 80 81 orbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) )
83 79 82 ralprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
84 25 83 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
85 84 imbi1d ⊢ ( 𝜑 → ( ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ↔ ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
86 85 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ↔ ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
87 eqid ⊢ 𝐴 = 𝐴
88 87 orci ⊢ ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 )
89 eqid ⊢ 𝐵 = 𝐵
90 89 olci ⊢ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 )
91 pm5.5 ⊢ ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → ( ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ↔ { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
92 88 90 91 mp2an ⊢ ( ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ↔ { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
93 10 11 pm3.2i ⊢ ( 𝑎 ∈ V ∧ 𝑏 ∈ V )
94 preq12bg ⊢ ( ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) ) )
95 93 25 94 sylancr ⊢ ( 𝜑 → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) ) )
96 95 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) ) )
97 96 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ↔ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) ) )
98 eqeq12 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 = 𝑏 ↔ 𝐴 = 𝐵 ) )
99 98 necon3bid ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝑏 ↔ 𝐴 ≠ 𝐵 ) )
100 99 biimpd ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( 𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵 ) )
101 eqeq12 ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) → ( 𝑎 = 𝑏 ↔ 𝐵 = 𝐴 ) )
102 101 necon3bid ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) → ( 𝑎 ≠ 𝑏 ↔ 𝐵 ≠ 𝐴 ) )
103 102 biimpd ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) → ( 𝑎 ≠ 𝑏 → 𝐵 ≠ 𝐴 ) )
104 necom ⊢ ( 𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴 )
105 103 104 syl6ibr ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) → ( 𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵 ) )
106 100 105 jaoi ⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) → ( 𝑎 ≠ 𝑏 → 𝐴 ≠ 𝐵 ) )
107 106 com12 ⊢ ( 𝑎 ≠ 𝑏 → ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) → 𝐴 ≠ 𝐵 ) )
108 107 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ∨ ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐴 ) ) → 𝐴 ≠ 𝐵 ) )
109 97 108 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } → 𝐴 ≠ 𝐵 ) )
110 109 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } → 𝐴 ≠ 𝐵 ) )
111 92 110 syl5bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ( ( ( 𝐴 = 𝐴 ∨ 𝐴 = 𝐵 ) ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) → 𝐴 ≠ 𝐵 ) )
112 86 111 sylbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) → 𝐴 ≠ 𝐵 ) )
113 76 112 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ) → ( ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) → 𝐴 ≠ 𝐵 ) )
114 113 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) → ( ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) → 𝐴 ≠ 𝐵 ) ) )
115 114 impd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ∧ ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝑎 , 𝑏 } = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) )
116 24 115 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) )
117 116 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) ) )
118 117 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑝 = { 𝑎 , 𝑏 } ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) ) )
119 8 118 syl5bi ⊢ ( 𝜑 → ( 𝑝 ∈ 𝑃 → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) ) )
120 119 imp ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝑃 ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) )
121 120 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑞 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑞 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑞 ) ) → 𝐴 ≠ 𝐵 ) )
122 5 121 syl5bi ⊢ ( 𝜑 → ( ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝐴 ≠ 𝐵 ) )
123 27 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 )
124 hashprg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
125 25 124 syl ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 ↔ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
126 125 biimpd ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
127 126 imp ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 )
128 123 127 jca ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝐴 , 𝐵 } ) = 2 ) )
129 128 70 sylibr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ∈ 𝑃 )
130 raleq ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
131 eqeq1 ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( 𝑝 = 𝑦 ↔ { 𝐴 , 𝐵 } = 𝑦 ) )
132 131 imbi2d ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
133 132 ralbidv ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
134 130 133 anbi12d ⊢ ( 𝑝 = { 𝐴 , 𝐵 } → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) ) )
135 134 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑝 = { 𝐴 , 𝐵 } ) → ( ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) ) )
136 vex ⊢ 𝑥 ∈ V
137 136 elpr ⊢ ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
138 137 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 } ↔ ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
139 138 biimpd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑥 ∈ { 𝐴 , 𝐵 } → ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
140 139 imp ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑥 ∈ { 𝐴 , 𝐵 } ) → ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
141 140 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
142 3 eleq2i ⊢ ( 𝑦 ∈ 𝑃 ↔ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
143 elss2prb ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) )
144 142 143 bitri ⊢ ( 𝑦 ∈ 𝑃 ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) )
145 prid1g ⊢ ( 𝑎 ∈ 𝑉 → 𝑎 ∈ { 𝑎 , 𝑏 } )
146 145 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ { 𝑎 , 𝑏 } )
147 146 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → 𝑎 ∈ { 𝑎 , 𝑏 } )
148 eleq2 ⊢ ( 𝑦 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ 𝑦 ↔ 𝑎 ∈ { 𝑎 , 𝑏 } ) )
149 148 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( 𝑎 ∈ 𝑦 ↔ 𝑎 ∈ { 𝑎 , 𝑏 } ) )
150 147 149 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → 𝑎 ∈ 𝑦 )
151 14 rspcv ⊢ ( 𝑎 ∈ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) )
152 150 151 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) )
153 prid2g ⊢ ( 𝑏 ∈ 𝑉 → 𝑏 ∈ { 𝑎 , 𝑏 } )
154 153 ad2antll ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ { 𝑎 , 𝑏 } )
155 154 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ { 𝑎 , 𝑏 } )
156 eleq2 ⊢ ( 𝑦 = { 𝑎 , 𝑏 } → ( 𝑏 ∈ 𝑦 ↔ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
157 156 ad2antll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( 𝑏 ∈ 𝑦 ↔ 𝑏 ∈ { 𝑎 , 𝑏 } ) )
158 155 157 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → 𝑏 ∈ 𝑦 )
159 17 rspcv ⊢ ( 𝑏 ∈ 𝑦 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) )
160 158 159 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ) )
161 simplrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ∧ ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) ) → 𝑦 = { 𝑎 , 𝑏 } )
162 eqtr3 ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐴 ) → 𝑎 = 𝑏 )
163 eqneqall ⊢ ( 𝑎 = 𝑏 → ( 𝑎 ≠ 𝑏 → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
164 163 com12 ⊢ ( 𝑎 ≠ 𝑏 → ( 𝑎 = 𝑏 → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
165 164 ad2antrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( 𝑎 = 𝑏 → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
166 165 com12 ⊢ ( 𝑎 = 𝑏 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
167 162 166 syl ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐴 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
168 167 ex ⊢ ( 𝑎 = 𝐴 → ( 𝑏 = 𝐴 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
169 52 a1d ⊢ ( ( 𝑏 = 𝐴 ∧ 𝑎 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
170 169 expcom ⊢ ( 𝑎 = 𝐵 → ( 𝑏 = 𝐴 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
171 168 170 jaoi ⊢ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( 𝑏 = 𝐴 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
172 171 com12 ⊢ ( 𝑏 = 𝐴 → ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
173 44 a1d ⊢ ( ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
174 173 ex ⊢ ( 𝑎 = 𝐴 → ( 𝑏 = 𝐵 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
175 eqtr3 ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐵 ) → 𝑎 = 𝑏 )
176 175 166 syl ⊢ ( ( 𝑎 = 𝐵 ∧ 𝑏 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
177 176 ex ⊢ ( 𝑎 = 𝐵 → ( 𝑏 = 𝐵 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
178 174 177 jaoi ⊢ ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( 𝑏 = 𝐵 → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
179 178 com12 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
180 172 179 jaoi ⊢ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) ) )
181 180 imp ⊢ ( ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ∧ ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) → ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } ) )
182 181 impcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ∧ ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) ) → { 𝑎 , 𝑏 } = { 𝐴 , 𝐵 } )
183 161 182 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) ∧ ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) ∧ ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) ) ) → { 𝐴 , 𝐵 } = 𝑦 )
184 183 exp32 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( ( 𝑏 = 𝐴 ∨ 𝑏 = 𝐵 ) → ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
185 160 184 syld ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → ( ( 𝑎 = 𝐴 ∨ 𝑎 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
186 152 185 mpdd ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) )
187 186 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
188 187 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ( 𝑎 ≠ 𝑏 ∧ 𝑦 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
189 144 188 syl5bi ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝑦 ∈ 𝑃 → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
190 189 imp ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑦 ∈ 𝑃 ) → ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) )
191 190 ralrimiva ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) )
192 141 191 jca ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ∀ 𝑥 ∈ { 𝐴 , 𝐵 } ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → { 𝐴 , 𝐵 } = 𝑦 ) ) )
193 129 135 192 rspcedvd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑝 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ) )
194 raleq ⊢ ( 𝑝 = 𝑦 → ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
195 194 reu8 ⊢ ( ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ ∃ 𝑝 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ∧ ∀ 𝑦 ∈ 𝑃 ( ∀ 𝑥 ∈ 𝑦 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) → 𝑝 = 𝑦 ) ) )
196 193 195 sylibr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) )
197 196 ex ⊢ ( 𝜑 → ( 𝐴 ≠ 𝐵 → ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ) )
198 122 197 impbid ⊢ ( 𝜑 → ( ∃! 𝑝 ∈ 𝑃 ∀ 𝑥 ∈ 𝑝 ( 𝑥 = 𝐴 ∨ 𝑥 = 𝐵 ) ↔ 𝐴 ≠ 𝐵 ) )