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	⊢ ( 𝜑 → 𝜂 )