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 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ ( 𝑍 ∖ { 𝑎 } ) { ⟨“ 𝑎 𝐵 𝑐 ”⟩ } )