Metamath Proof Explorer

Theorem trsp2cyc

Description: Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023)

Ref Expression
Hypotheses trsp2cyc.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
trsp2cyc.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
Assertion trsp2cyc ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ∃ 𝑖 ∈ 𝐷 ∃ 𝑗 ∈ 𝐷 ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) )

Proof

Step Hyp Ref Expression
1 trsp2cyc.t ⊢ 𝑇 = ran ( pmTrsp ‘ 𝐷 )
2 trsp2cyc.c ⊢ 𝐶 = ( toCyc ‘ 𝐷 )
3 simplr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } )
4 breq1 ⊢ ( 𝑦 = 𝑝 → ( 𝑦 ≈ 2o ↔ 𝑝 ≈ 2o ) )
5 4 elrab ⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↔ ( 𝑝 ∈ 𝒫 𝐷 ∧ 𝑝 ≈ 2o ) )
6 3 5 sylib ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ( 𝑝 ∈ 𝒫 𝐷 ∧ 𝑝 ≈ 2o ) )
7 6 simprd ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → 𝑝 ≈ 2o )
8 en2 ⊢ ( 𝑝 ≈ 2o → ∃ 𝑖 ∃ 𝑗 𝑝 = { 𝑖 , 𝑗 } )
9 7 8 syl ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ∃ 𝑖 ∃ 𝑗 𝑝 = { 𝑖 , 𝑗 } )
10 6 simpld ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → 𝑝 ∈ 𝒫 𝐷 )
11 10 elpwid ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → 𝑝 ⊆ 𝐷 )
12 11 adantr ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑝 ⊆ 𝐷 )
13 vex ⊢ 𝑖 ∈ V
14 13 prid1 ⊢ 𝑖 ∈ { 𝑖 , 𝑗 }
15 simpr ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑝 = { 𝑖 , 𝑗 } )
16 14 15 eleqtrrid ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑖 ∈ 𝑝 )
17 12 16 sseldd ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑖 ∈ 𝐷 )
18 vex ⊢ 𝑗 ∈ V
19 18 prid2 ⊢ 𝑗 ∈ { 𝑖 , 𝑗 }
20 19 15 eleqtrrid ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑗 ∈ 𝑝 )
21 12 20 sseldd ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑗 ∈ 𝐷 )
22 7 adantr ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑝 ≈ 2o )
23 15 22 eqbrtrrd ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → { 𝑖 , 𝑗 } ≈ 2o )
24 pr2ne ⊢ ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) → ( { 𝑖 , 𝑗 } ≈ 2o ↔ 𝑖 ≠ 𝑗 ) )
25 24 biimpa ⊢ ( ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ { 𝑖 , 𝑗 } ≈ 2o ) → 𝑖 ≠ 𝑗 )
26 17 21 23 25 syl21anc ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑖 ≠ 𝑗 )
27 simplr ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
28 simp-4l ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝐷 ∈ 𝑉 )
29 eqid ⊢ ( pmTrsp ‘ 𝐷 ) = ( pmTrsp ‘ 𝐷 )
30 29 pmtrval ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑝 ⊆ 𝐷 ∧ 𝑝 ≈ 2o ) → ( ( pmTrsp ‘ 𝐷 ) ‘ 𝑝 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
31 28 12 22 30 syl3anc ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ 𝑝 ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
32 15 fveq2d ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( ( pmTrsp ‘ 𝐷 ) ‘ 𝑝 ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑖 , 𝑗 } ) )
33 27 31 32 3eqtr2d ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑃 = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑖 , 𝑗 } ) )
34 2 28 17 21 26 29 cycpm2tr ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) = ( ( pmTrsp ‘ 𝐷 ) ‘ { 𝑖 , 𝑗 } ) )
35 33 34 eqtr4d ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) )
36 26 35 jca ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) )
37 17 21 36 jca31 ⊢ ( ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ∧ 𝑝 = { 𝑖 , 𝑗 } ) → ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ) )
38 37 ex ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ( 𝑝 = { 𝑖 , 𝑗 } → ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ) ) )
39 38 2eximdv ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ( ∃ 𝑖 ∃ 𝑗 𝑝 = { 𝑖 , 𝑗 } → ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ) ) )
40 9 39 mpd ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ) )
41 r2ex ⊢ ( ∃ 𝑖 ∈ 𝐷 ∃ 𝑗 ∈ 𝐷 ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ↔ ∃ 𝑖 ∃ 𝑗 ( ( 𝑖 ∈ 𝐷 ∧ 𝑗 ∈ 𝐷 ) ∧ ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) ) )
42 40 41 sylibr ⊢ ( ( ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) ∧ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ) ∧ 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) → ∃ 𝑖 ∈ 𝐷 ∃ 𝑗 ∈ 𝐷 ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) )
43 simpr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → 𝑃 ∈ 𝑇 )
44 29 pmtrfval ⊢ ( 𝐷 ∈ 𝑉 → ( pmTrsp ‘ 𝐷 ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
45 44 adantr ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ( pmTrsp ‘ 𝐷 ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
46 45 rneqd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ran ( pmTrsp ‘ 𝐷 ) = ran ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
47 1 46 syl5eq ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → 𝑇 = ran ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
48 43 47 eleqtrd ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → 𝑃 ∈ ran ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
49 eqid ⊢ ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) = ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
50 49 elrnmpt ⊢ ( 𝑃 ∈ 𝑇 → ( 𝑃 ∈ ran ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ↔ ∃ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
51 50 adantl ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ( 𝑃 ∈ ran ( 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) ↔ ∃ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) ) )
52 48 51 mpbid ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ∃ 𝑝 ∈ { 𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o } 𝑃 = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ 𝑝 , ∪ ( 𝑝 ∖ { 𝑧 } ) , 𝑧 ) ) )
53 42 52 r19.29a ⊢ ( ( 𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇 ) → ∃ 𝑖 ∈ 𝐷 ∃ 𝑗 ∈ 𝐷 ( 𝑖 ≠ 𝑗 ∧ 𝑃 = ( 𝐶 ‘ ⟨“ 𝑖 𝑗 ”⟩ ) ) )