This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌 ) ) ∧ ( 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ∧ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) ) ) → ( ⟨“ 𝑎 𝐵 𝑐 ”⟩ = ⟨“ 𝑑 𝐵 𝑒 ”⟩ → 𝑎 = 𝑑 ) )
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 biimtrid ⊢ ( ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌 ) ) ) ∧ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) ) → ( 𝑠 ∈ { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } → ( 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) → ¬ 𝑠 = ⟨“ 𝑑 𝐵 𝑒 ”⟩ ) ) )
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 biimtrid ⊢ ( ( ¬ 𝑎 = 𝑑 ∧ ( 𝐵 ∈ 𝑋 ∧ ( 𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌 ) ) ) → ( 𝑠 ∈ ∪ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } → ¬ 𝑠 ∈ ∪ 𝑒 ∈ ( 𝑍 ∖ { 𝑑 } ) { ⟨“ 𝑑 𝐵 𝑒 ”⟩ } ) )
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 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } )