Metamath Proof Explorer


Theorem s3iunsndisj

Description: The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021)

Ref Expression
Assertion s3iunsndisj ( 𝐵𝑋Disj 𝑎𝑌 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } )

Proof

Step Hyp Ref Expression
1 orc ( 𝑎 = 𝑑 → ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) )
2 1 a1d ( 𝑎 = 𝑑 → ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) ) )
3 eliun ( 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ↔ ∃ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } )
4 velsn ( 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ↔ 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ )
5 eqeq1 ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ( 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ↔ ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) )
6 5 adantl ( ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) ∧ 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) → ( 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ↔ ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) )
7 s3cli ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∈ Word V
8 elex ( 𝐵𝑋𝐵 ∈ V )
9 elex ( 𝑑𝑌𝑑 ∈ V )
10 9 adantl ( ( 𝑎𝑌𝑑𝑌 ) → 𝑑 ∈ V )
11 8 10 anim12ci ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( 𝑑 ∈ V ∧ 𝐵 ∈ V ) )
12 elex ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → 𝑒 ∈ V )
13 12 adantl ( ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → 𝑒 ∈ V )
14 11 13 anim12i ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) → ( ( 𝑑 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑒 ∈ V ) )
15 df-3an ( ( 𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V ) ↔ ( ( 𝑑 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑒 ∈ V ) )
16 14 15 sylibr ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) → ( 𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V ) )
17 eqwrds3 ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∈ Word V ∧ ( 𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V ) ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ↔ ( ( ♯ ‘ ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑒 ) ) ) )
18 7 16 17 sylancr ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ↔ ( ( ♯ ‘ ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑒 ) ) ) )
19 s3fv0 ( 𝑎 ∈ V → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑎 )
20 19 elv ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑎
21 simp1 ( ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑒 ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 )
22 20 21 eqtr3id ( ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑒 ) → 𝑎 = 𝑑 )
23 22 adantl ( ( ( ♯ ‘ ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) = 3 ∧ ( ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 0 ) = 𝑑 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 1 ) = 𝐵 ∧ ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ ‘ 2 ) = 𝑒 ) ) → 𝑎 = 𝑑 )
24 18 23 syl6bi ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ → 𝑎 = 𝑑 ) )
25 24 adantr ( ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) ∧ 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ → 𝑎 = 𝑑 ) )
26 6 25 sylbid ( ( ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) ∧ 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ ) → ( 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ → 𝑎 = 𝑑 ) )
27 26 ancoms ( ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∧ ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) ) → ( 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ → 𝑎 = 𝑑 ) )
28 27 con3d ( ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ ∧ ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) ) → ( ¬ 𝑎 = 𝑑 → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) )
29 28 exp32 ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → ( ¬ 𝑎 = 𝑑 → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) ) )
30 29 com14 ( ¬ 𝑎 = 𝑑 → ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) ) )
31 30 imp ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) )
32 31 expd ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) ) )
33 32 com34 ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) → ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) ) )
34 33 imp ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) → ( 𝑠 = ⟨“ 𝑎 𝐵 𝑐 ”⟩ → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) )
35 4 34 syl5bi ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) → ( 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) )
36 35 imp ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ) → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) )
37 36 imp ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ )
38 velsn ( 𝑠 ∈ { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } ↔ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ )
39 37 38 sylnibr ( ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) → ¬ 𝑠 ∈ { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
40 39 nrexdv ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ) → ¬ ∃ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) 𝑠 ∈ { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
41 eliun ( 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } ↔ ∃ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) 𝑠 ∈ { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
42 40 41 sylnibr ( ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) ∧ 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ) → ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
43 42 rexlimdva2 ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( ∃ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } → ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } ) )
44 3 43 syl5bi ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } → ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } ) )
45 44 ralrimiv ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ∀ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
46 eqidd ( 𝑐 = 𝑒𝑑 = 𝑑 )
47 eqidd ( 𝑐 = 𝑒𝐵 = 𝐵 )
48 id ( 𝑐 = 𝑒𝑐 = 𝑒 )
49 46 47 48 s3eqd ( 𝑐 = 𝑒 → ⟨“ 𝑑 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ )
50 49 sneqd ( 𝑐 = 𝑒 → { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } = { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
51 50 cbviunv 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } = 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ }
52 51 eleq2i ( 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ↔ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
53 52 notbii ( ¬ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ↔ ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
54 53 ralbii ( ∀ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ¬ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ↔ ∀ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ¬ 𝑠 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } )
55 45 54 sylibr ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ∀ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ¬ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } )
56 disj ( ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ↔ ∀ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ¬ 𝑠 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } )
57 55 56 sylibr ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ )
58 57 olcd ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) ) → ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) )
59 58 ex ( ¬ 𝑎 = 𝑑 → ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) ) )
60 2 59 pm2.61i ( ( 𝐵𝑋 ∧ ( 𝑎𝑌𝑑𝑌 ) ) → ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) )
61 60 ralrimivva ( 𝐵𝑋 → ∀ 𝑎𝑌𝑑𝑌 ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) )
62 sneq ( 𝑎 = 𝑑 → { 𝑎 } = { 𝑑 } )
63 62 difeq2d ( 𝑎 = 𝑑 → ( 𝑍 ∖ { 𝑎 } ) = ( 𝑍 ∖ { 𝑑 } ) )
64 id ( 𝑎 = 𝑑𝑎 = 𝑑 )
65 eqidd ( 𝑎 = 𝑑𝐵 = 𝐵 )
66 eqidd ( 𝑎 = 𝑑𝑐 = 𝑐 )
67 64 65 66 s3eqd ( 𝑎 = 𝑑 → ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑐 ”⟩ )
68 67 sneqd ( 𝑎 = 𝑑 → { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } = { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } )
69 63 68 disjiunb ( Disj 𝑎𝑌 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ↔ ∀ 𝑎𝑌𝑑𝑌 ( 𝑎 = 𝑑 ∨ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } ∩ 𝑐 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑐 ”⟩ } ) = ∅ ) )
70 61 69 sylibr ( 𝐵𝑋Disj 𝑎𝑌 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } )