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

Metamath Proof Explorer

Theorem findcard2d

Description: Deduction version of findcard2 . (Contributed by SO, 16-Jul-2018)

Ref Expression
Hypotheses findcard2d.ch ⊢ ( 𝑥 = ∅ → ( 𝜓 ↔ 𝜒 ) )
findcard2d.th ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
findcard2d.ta ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜓 ↔ 𝜏 ) )
findcard2d.et ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
findcard2d.z ⊢ ( 𝜑 → 𝜒 )
findcard2d.i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝜃 → 𝜏 ) )
findcard2d.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion findcard2d ( 𝜑 → 𝜂 )

Proof

Step Hyp Ref Expression
1 findcard2d.ch ⊢ ( 𝑥 = ∅ → ( 𝜓 ↔ 𝜒 ) )
2 findcard2d.th ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜃 ) )
3 findcard2d.ta ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝜓 ↔ 𝜏 ) )
4 findcard2d.et ⊢ ( 𝑥 = 𝐴 → ( 𝜓 ↔ 𝜂 ) )
5 findcard2d.z ⊢ ( 𝜑 → 𝜒 )
6 findcard2d.i ⊢ ( ( 𝜑 ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝜃 → 𝜏 ) )
7 findcard2d.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
8 ssid ⊢ 𝐴 ⊆ 𝐴
9 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝐴 ∈ Fin )
10 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
11 10 anbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ ∅ ⊆ 𝐴 ) ) )
12 11 1 imbi12d ⊢ ( 𝑥 = ∅ → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ∅ ⊆ 𝐴 ) → 𝜒 ) ) )
13 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
14 13 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) ) )
15 14 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝜓 ) ↔ ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝜃 ) ) )
16 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ⊆ 𝐴 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) )
17 16 anbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) )
18 17 3 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝜓 ) ↔ ( ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → 𝜏 ) ) )
19 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
20 19 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) ↔ ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) ) )
21 20 4 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ⊆ 𝐴 ) → 𝜓 ) ↔ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝜂 ) ) )
22 5 adantr ⊢ ( ( 𝜑 ∧ ∅ ⊆ 𝐴 ) → 𝜒 )
23 simprl ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝜑 )
24 simprr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
25 24 unssad ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑦 ⊆ 𝐴 )
26 23 25 jca ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) )
27 id ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 )
28 vsnid ⊢ 𝑧 ∈ { 𝑧 }
29 elun2 ⊢ ( 𝑧 ∈ { 𝑧 } → 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) )
30 28 29 mp1i ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑧 ∈ ( 𝑦 ∪ { 𝑧 } ) )
31 27 30 sseldd ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 → 𝑧 ∈ 𝐴 )
32 31 ad2antll ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
33 simplr ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ¬ 𝑧 ∈ 𝑦 )
34 32 33 eldifd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) )
35 23 25 34 6 syl12anc ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( 𝜃 → 𝜏 ) )
36 26 35 embantd ⊢ ( ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) ∧ ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) ) → ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝜃 ) → 𝜏 ) )
37 36 ex ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝜃 ) → 𝜏 ) ) )
38 37 com23 ⊢ ( ( 𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦 ) → ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝐴 ) → 𝜃 ) → ( ( 𝜑 ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝐴 ) → 𝜏 ) ) )
39 12 15 18 21 22 38 findcard2s ⊢ ( 𝐴 ∈ Fin → ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝜂 ) )
40 9 39 mpcom ⊢ ( ( 𝜑 ∧ 𝐴 ⊆ 𝐴 ) → 𝜂 )
41 8 40 mpan2 ⊢ ( 𝜑 → 𝜂 )