Metamath Proof Explorer

Theorem s3sndisj

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

Ref Expression
Assertion s3sndisj 
|- ( ( A e. X /\ B e. Y ) -> Disj_ c e. Z { <" A B c "> } )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( c = d -> ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) )
2 1 a1d 
 |-  ( c = d -> ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) ) )
3 s3cli 
 |-  <" A B c "> e. Word _V
4 elex 
 |-  ( A e. X -> A e. _V )
5 elex 
 |-  ( B e. Y -> B e. _V )
6 4 5 anim12i 
 |-  ( ( A e. X /\ B e. Y ) -> ( A e. _V /\ B e. _V ) )
7 elex 
 |-  ( d e. Z -> d e. _V )
8 7 adantl 
 |-  ( ( c e. Z /\ d e. Z ) -> d e. _V )
9 6 8 anim12i 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( ( A e. _V /\ B e. _V ) /\ d e. _V ) )
10 df-3an 
 |-  ( ( A e. _V /\ B e. _V /\ d e. _V ) <-> ( ( A e. _V /\ B e. _V ) /\ d e. _V ) )
11 9 10 sylibr 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( A e. _V /\ B e. _V /\ d e. _V ) )
12 eqwrds3 
 |-  ( ( <" A B c "> e. Word _V /\ ( A e. _V /\ B e. _V /\ d e. _V ) ) -> ( <" A B c "> = <" A B d "> <-> ( ( # ` <" A B c "> ) = 3 /\ ( ( <" A B c "> ` 0 ) = A /\ ( <" A B c "> ` 1 ) = B /\ ( <" A B c "> ` 2 ) = d ) ) ) )
13 3 11 12 sylancr 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( <" A B c "> = <" A B d "> <-> ( ( # ` <" A B c "> ) = 3 /\ ( ( <" A B c "> ` 0 ) = A /\ ( <" A B c "> ` 1 ) = B /\ ( <" A B c "> ` 2 ) = d ) ) ) )
14 s3fv2 
 |-  ( c e. _V -> ( <" A B c "> ` 2 ) = c )
15 14 elv 
 |-  ( <" A B c "> ` 2 ) = c
16 simp3 
 |-  ( ( ( <" A B c "> ` 0 ) = A /\ ( <" A B c "> ` 1 ) = B /\ ( <" A B c "> ` 2 ) = d ) -> ( <" A B c "> ` 2 ) = d )
17 15 16 eqtr3id 
 |-  ( ( ( <" A B c "> ` 0 ) = A /\ ( <" A B c "> ` 1 ) = B /\ ( <" A B c "> ` 2 ) = d ) -> c = d )
18 17 adantl 
 |-  ( ( ( # ` <" A B c "> ) = 3 /\ ( ( <" A B c "> ` 0 ) = A /\ ( <" A B c "> ` 1 ) = B /\ ( <" A B c "> ` 2 ) = d ) ) -> c = d )
19 13 18 syl6bi 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( <" A B c "> = <" A B d "> -> c = d ) )
20 19 con3rr3 
 |-  ( -. c = d -> ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> -. <" A B c "> = <" A B d "> ) )
21 20 imp 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) ) -> -. <" A B c "> = <" A B d "> )
22 21 neqned 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) ) -> <" A B c "> =/= <" A B d "> )
23 disjsn2 
 |-  ( <" A B c "> =/= <" A B d "> -> ( { <" A B c "> } i^i { <" A B d "> } ) = (/) )
24 22 23 syl 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) ) -> ( { <" A B c "> } i^i { <" A B d "> } ) = (/) )
25 24 olcd 
 |-  ( ( -. c = d /\ ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) ) -> ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) )
26 25 ex 
 |-  ( -. c = d -> ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) ) )
27 2 26 pm2.61i 
 |-  ( ( ( A e. X /\ B e. Y ) /\ ( c e. Z /\ d e. Z ) ) -> ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) )
28 27 ralrimivva 
 |-  ( ( A e. X /\ B e. Y ) -> A. c e. Z A. d e. Z ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) )
29 eqidd 
 |-  ( c = d -> A = A )
30 eqidd 
 |-  ( c = d -> B = B )
31 id 
 |-  ( c = d -> c = d )
32 29 30 31 s3eqd 
 |-  ( c = d -> <" A B c "> = <" A B d "> )
33 32 sneqd 
 |-  ( c = d -> { <" A B c "> } = { <" A B d "> } )
34 33 disjor 
 |-  ( Disj_ c e. Z { <" A B c "> } <-> A. c e. Z A. d e. Z ( c = d \/ ( { <" A B c "> } i^i { <" A B d "> } ) = (/) ) )
35 28 34 sylibr 
 |-  ( ( A e. X /\ B e. Y ) -> Disj_ c e. Z { <" A B c "> } )