Metamath Proof Explorer


Theorem boxcutc

Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion boxcutc ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) → ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) = X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eldifi ( 𝑧 ∈ ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) → 𝑧X 𝑘𝐴 𝐵 )
2 1 adantl ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧 ∈ ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) → 𝑧X 𝑘𝐴 𝐵 )
3 sseq1 ( ( 𝐵𝐶 ) = if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) → ( ( 𝐵𝐶 ) ⊆ 𝐵 ↔ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ 𝐵 ) )
4 sseq1 ( 𝐵 = if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) → ( 𝐵𝐵 ↔ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ 𝐵 ) )
5 difss ( 𝐵𝐶 ) ⊆ 𝐵
6 ssid 𝐵𝐵
7 3 4 5 6 keephyp if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ 𝐵
8 7 rgenw 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ 𝐵
9 ss2ixp ( ∀ 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ X 𝑘𝐴 𝐵 )
10 8 9 mp1i ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) → X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ⊆ X 𝑘𝐴 𝐵 )
11 10 sselda ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) → 𝑧X 𝑘𝐴 𝐵 )
12 vex 𝑧 ∈ V
13 12 elixp ( 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
14 ixpfn ( 𝑧X 𝑘𝐴 𝐵𝑧 Fn 𝐴 )
15 14 adantl ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → 𝑧 Fn 𝐴 )
16 15 biantrurd ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
17 13 16 bitr4id ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
18 17 notbid ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
19 rexnal ( ∃ 𝑘𝐴 ¬ ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) )
20 eleq2 ( ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) = if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) → ( ( 𝑧𝑚 ) ∈ ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) ↔ ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) )
21 eleq2 ( 𝑚 / 𝑘 𝐵 = if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) → ( ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 ↔ ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) )
22 eleq2 ( 𝑙 / 𝑘 𝐶 = if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) → ( ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐶 ↔ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) )
23 eleq2 ( 𝑙 / 𝑘 𝐵 = if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) → ( ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 ↔ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) )
24 simpl ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) → 𝑋𝐴 )
25 12 elixp ( 𝑧X 𝑘𝐴 𝐵 ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ 𝐵 ) )
26 25 simprbi ( 𝑧X 𝑘𝐴 𝐵 → ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ 𝐵 )
27 nfv 𝑙 ( 𝑧𝑘 ) ∈ 𝐵
28 nfcsb1v 𝑘 𝑙 / 𝑘 𝐵
29 28 nfel2 𝑘 ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵
30 fveq2 ( 𝑘 = 𝑙 → ( 𝑧𝑘 ) = ( 𝑧𝑙 ) )
31 csbeq1a ( 𝑘 = 𝑙𝐵 = 𝑙 / 𝑘 𝐵 )
32 30 31 eleq12d ( 𝑘 = 𝑙 → ( ( 𝑧𝑘 ) ∈ 𝐵 ↔ ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 ) )
33 27 29 32 cbvralw ( ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ 𝐵 ↔ ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 )
34 26 33 sylib ( 𝑧X 𝑘𝐴 𝐵 → ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 )
35 fveq2 ( 𝑙 = 𝑋 → ( 𝑧𝑙 ) = ( 𝑧𝑋 ) )
36 csbeq1 ( 𝑙 = 𝑋 𝑙 / 𝑘 𝐵 = 𝑋 / 𝑘 𝐵 )
37 35 36 eleq12d ( 𝑙 = 𝑋 → ( ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 ↔ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐵 ) )
38 37 rspcva ( ( 𝑋𝐴 ∧ ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 ) → ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐵 )
39 24 34 38 syl2an ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐵 )
40 neldif ( ( ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐵 ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) → ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 )
41 39 40 sylan ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) → ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 )
42 41 adantr ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) → ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 )
43 csbeq1 ( 𝑙 = 𝑋 𝑙 / 𝑘 𝐶 = 𝑋 / 𝑘 𝐶 )
44 35 43 eleq12d ( 𝑙 = 𝑋 → ( ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐶 ↔ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 ) )
45 42 44 syl5ibrcom ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) → ( 𝑙 = 𝑋 → ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐶 ) )
46 45 imp ( ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) ∧ 𝑙 = 𝑋 ) → ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐶 )
47 34 ad2antlr ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) → ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 )
48 47 r19.21bi ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) → ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 )
49 48 adantr ( ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) ∧ ¬ 𝑙 = 𝑋 ) → ( 𝑧𝑙 ) ∈ 𝑙 / 𝑘 𝐵 )
50 22 23 46 49 ifbothda ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) ∧ 𝑙𝐴 ) → ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
51 50 ralrimiva ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) → ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
52 dfral2 ( ∀ 𝑙𝐴 ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ↔ ¬ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
53 51 52 sylib ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) → ¬ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
54 53 ex ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ¬ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) → ¬ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) )
55 54 con4d ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) → ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) )
56 55 imp ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) → ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
57 56 adantr ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) → ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
58 fveq2 ( 𝑚 = 𝑋 → ( 𝑧𝑚 ) = ( 𝑧𝑋 ) )
59 csbeq1 ( 𝑚 = 𝑋 𝑚 / 𝑘 𝐵 = 𝑋 / 𝑘 𝐵 )
60 csbeq1 ( 𝑚 = 𝑋 𝑚 / 𝑘 𝐶 = 𝑋 / 𝑘 𝐶 )
61 59 60 difeq12d ( 𝑚 = 𝑋 → ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) = ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
62 58 61 eleq12d ( 𝑚 = 𝑋 → ( ( 𝑧𝑚 ) ∈ ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) ↔ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) )
63 57 62 syl5ibrcom ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) → ( 𝑚 = 𝑋 → ( 𝑧𝑚 ) ∈ ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) ) )
64 63 imp ( ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) ∧ 𝑚 = 𝑋 ) → ( 𝑧𝑚 ) ∈ ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) )
65 nfv 𝑚 ( 𝑧𝑘 ) ∈ 𝐵
66 nfcsb1v 𝑘 𝑚 / 𝑘 𝐵
67 66 nfel2 𝑘 ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵
68 fveq2 ( 𝑘 = 𝑚 → ( 𝑧𝑘 ) = ( 𝑧𝑚 ) )
69 csbeq1a ( 𝑘 = 𝑚𝐵 = 𝑚 / 𝑘 𝐵 )
70 68 69 eleq12d ( 𝑘 = 𝑚 → ( ( 𝑧𝑘 ) ∈ 𝐵 ↔ ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 ) )
71 65 67 70 cbvralw ( ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ 𝐵 ↔ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 )
72 26 71 sylib ( 𝑧X 𝑘𝐴 𝐵 → ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 )
73 72 ad2antlr ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) → ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 )
74 73 r19.21bi ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) → ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 )
75 74 adantr ( ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) ∧ ¬ 𝑚 = 𝑋 ) → ( 𝑧𝑚 ) ∈ 𝑚 / 𝑘 𝐵 )
76 20 21 64 75 ifbothda ( ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) ∧ 𝑚𝐴 ) → ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) )
77 76 ralrimiva ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) → ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) )
78 simpll ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → 𝑋𝐴 )
79 iftrue ( 𝑚 = 𝑋 → if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) = ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) )
80 79 61 eqtrd ( 𝑚 = 𝑋 → if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) = ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
81 58 80 eleq12d ( 𝑚 = 𝑋 → ( ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ↔ ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) ) )
82 81 rspcva ( ( 𝑋𝐴 ∧ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) → ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
83 78 82 sylan ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) → ( 𝑧𝑋 ) ∈ ( 𝑋 / 𝑘 𝐵 𝑋 / 𝑘 𝐶 ) )
84 83 eldifbd ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) → ¬ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 )
85 iftrue ( 𝑙 = 𝑋 → if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) = 𝑙 / 𝑘 𝐶 )
86 85 43 eqtrd ( 𝑙 = 𝑋 → if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) = 𝑋 / 𝑘 𝐶 )
87 35 86 eleq12d ( 𝑙 = 𝑋 → ( ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ↔ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 ) )
88 87 notbid ( 𝑙 = 𝑋 → ( ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ↔ ¬ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 ) )
89 88 rspcev ( ( 𝑋𝐴 ∧ ¬ ( 𝑧𝑋 ) ∈ 𝑋 / 𝑘 𝐶 ) → ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
90 78 84 89 syl2an2r ( ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) ∧ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) → ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
91 77 90 impbida ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ↔ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) )
92 nfv 𝑙 ¬ ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 )
93 nfv 𝑘 𝑙 = 𝑋
94 nfcsb1v 𝑘 𝑙 / 𝑘 𝐶
95 93 94 28 nfif 𝑘 if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 )
96 95 nfel2 𝑘 ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 )
97 96 nfn 𝑘 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 )
98 eqeq1 ( 𝑘 = 𝑙 → ( 𝑘 = 𝑋𝑙 = 𝑋 ) )
99 csbeq1a ( 𝑘 = 𝑙𝐶 = 𝑙 / 𝑘 𝐶 )
100 98 99 31 ifbieq12d ( 𝑘 = 𝑙 → if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) = if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
101 30 100 eleq12d ( 𝑘 = 𝑙 → ( ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) )
102 101 notbid ( 𝑘 = 𝑙 → ( ¬ ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) ) )
103 92 97 102 cbvrexw ( ∃ 𝑘𝐴 ¬ ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∃ 𝑙𝐴 ¬ ( 𝑧𝑙 ) ∈ if ( 𝑙 = 𝑋 , 𝑙 / 𝑘 𝐶 , 𝑙 / 𝑘 𝐵 ) )
104 nfv 𝑚 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 )
105 nfv 𝑘 𝑚 = 𝑋
106 nfcsb1v 𝑘 𝑚 / 𝑘 𝐶
107 66 106 nfdif 𝑘 ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 )
108 105 107 66 nfif 𝑘 if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 )
109 108 nfel2 𝑘 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 )
110 eqeq1 ( 𝑘 = 𝑚 → ( 𝑘 = 𝑋𝑚 = 𝑋 ) )
111 csbeq1a ( 𝑘 = 𝑚𝐶 = 𝑚 / 𝑘 𝐶 )
112 69 111 difeq12d ( 𝑘 = 𝑚 → ( 𝐵𝐶 ) = ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) )
113 110 112 69 ifbieq12d ( 𝑘 = 𝑚 → if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) = if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) )
114 68 113 eleq12d ( 𝑘 = 𝑚 → ( ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ↔ ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) ) )
115 104 109 114 cbvralw ( ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ↔ ∀ 𝑚𝐴 ( 𝑧𝑚 ) ∈ if ( 𝑚 = 𝑋 , ( 𝑚 / 𝑘 𝐵 𝑚 / 𝑘 𝐶 ) , 𝑚 / 𝑘 𝐵 ) )
116 91 103 115 3bitr4g ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ∃ 𝑘𝐴 ¬ ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) )
117 19 116 bitr3id ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ¬ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) )
118 18 117 bitrd ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) )
119 ibar ( 𝑧X 𝑘𝐴 𝐵 → ( ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧X 𝑘𝐴 𝐵 ∧ ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
120 119 adantl ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ↔ ( 𝑧X 𝑘𝐴 𝐵 ∧ ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ) )
121 15 biantrurd ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) ) )
122 118 120 121 3bitr3d ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( ( 𝑧X 𝑘𝐴 𝐵 ∧ ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) ) )
123 eldif ( 𝑧 ∈ ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ ( 𝑧X 𝑘𝐴 𝐵 ∧ ¬ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) )
124 12 elixp ( 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ↔ ( 𝑧 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑧𝑘 ) ∈ if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) )
125 122 123 124 3bitr4g ( ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) ∧ 𝑧X 𝑘𝐴 𝐵 ) → ( 𝑧 ∈ ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) ↔ 𝑧X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) ) )
126 2 11 125 eqrdav ( ( 𝑋𝐴 ∧ ∀ 𝑘𝐴 𝐶𝐵 ) → ( X 𝑘𝐴 𝐵X 𝑘𝐴 if ( 𝑘 = 𝑋 , 𝐶 , 𝐵 ) ) = X 𝑘𝐴 if ( 𝑘 = 𝑋 , ( 𝐵𝐶 ) , 𝐵 ) )