indcardi

Description: Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015)

	Ref	Expression
Hypotheses	indcardi.a	$⊢ φ \to A \in V$
	indcardi.b	$⊢ φ \to T \in dom card$
	indcardi.c	$⊢ (φ \land R ≼ T \land \forall y (S ≺ R \to χ)) \to ψ$
	indcardi.d	$⊢ x = y \to (ψ \leftrightarrow χ)$
	indcardi.e	$⊢ x = A \to (ψ \leftrightarrow θ)$
	indcardi.f	$⊢ x = y \to R = S$
	indcardi.g	$⊢ x = A \to R = T$
Assertion	indcardi	$⊢ φ \to θ$

Proof

Step	Hyp	Ref	Expression
1		indcardi.a	$⊢ φ \to A \in V$
2		indcardi.b	$⊢ φ \to T \in dom card$
3		indcardi.c	$⊢ (φ \land R ≼ T \land \forall y (S ≺ R \to χ)) \to ψ$
4		indcardi.d	$⊢ x = y \to (ψ \leftrightarrow χ)$
5		indcardi.e	$⊢ x = A \to (ψ \leftrightarrow θ)$
6		indcardi.f	$⊢ x = y \to R = S$
7		indcardi.g	$⊢ x = A \to R = T$
8		domrefg	$⊢ T \in dom card \to T ≼ T$
9	2 8	syl	$⊢ φ \to T ≼ T$
10		cardon	$⊢ card (T) \in On$
11	10	a1i	$⊢ φ \to card (T) \in On$
12		simpl1	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land \forall y (card (S) \in card (R) \to (S ≼ T \to χ))) \land R ≼ T) \to φ$
13		simpr	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land \forall y (card (S) \in card (R) \to (S ≼ T \to χ))) \land R ≼ T) \to R ≼ T$
14		simpr	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to S ≺ R$
15		simpl1	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to φ$
16	15 2	syl	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to T \in dom card$
17		sdomdom	$⊢ S ≺ R \to S ≼ R$
18		simpl3	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to R ≼ T$
19		domtr	$⊢ (S ≼ R \land R ≼ T) \to S ≼ T$
20	17 18 19	syl2an2	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to S ≼ T$
21		numdom	$⊢ (T \in dom card \land S ≼ T) \to S \in dom card$
22	16 20 21	syl2anc	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to S \in dom card$
23		numdom	$⊢ (T \in dom card \land R ≼ T) \to R \in dom card$
24	16 18 23	syl2anc	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to R \in dom card$
25		cardsdom2	$⊢ (S \in dom card \land R \in dom card) \to (card (S) \in card (R) \leftrightarrow S ≺ R)$
26	22 24 25	syl2anc	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to (card (S) \in card (R) \leftrightarrow S ≺ R)$
27	14 26	mpbird	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to card (S) \in card (R)$
28		id	$⊢ (card (S) \in card (R) \to (S ≼ T \to χ)) \to (card (S) \in card (R) \to (S ≼ T \to χ))$
29	28	com3l	$⊢ card (S) \in card (R) \to (S ≼ T \to ((card (S) \in card (R) \to (S ≼ T \to χ)) \to χ))$
30	27 20 29	sylc	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \land S ≺ R) \to ((card (S) \in card (R) \to (S ≼ T \to χ)) \to χ)$
31	30	ex	$⊢ (φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \to (S ≺ R \to ((card (S) \in card (R) \to (S ≼ T \to χ)) \to χ))$
32	31	com23	$⊢ (φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \to ((card (S) \in card (R) \to (S ≼ T \to χ)) \to (S ≺ R \to χ))$
33	32	alimdv	$⊢ (φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land R ≼ T) \to (\forall y (card (S) \in card (R) \to (S ≼ T \to χ)) \to \forall y (S ≺ R \to χ))$
34	33	3exp	$⊢ φ \to ((card (R) \in On \land card (R) \subseteq card (T)) \to (R ≼ T \to (\forall y (card (S) \in card (R) \to (S ≼ T \to χ)) \to \forall y (S ≺ R \to χ))))$
35	34	com34	$⊢ φ \to ((card (R) \in On \land card (R) \subseteq card (T)) \to (\forall y (card (S) \in card (R) \to (S ≼ T \to χ)) \to (R ≼ T \to \forall y (S ≺ R \to χ))))$
36	35	3imp1	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land \forall y (card (S) \in card (R) \to (S ≼ T \to χ))) \land R ≼ T) \to \forall y (S ≺ R \to χ)$
37	12 13 36 3	syl3anc	$⊢ ((φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land \forall y (card (S) \in card (R) \to (S ≼ T \to χ))) \land R ≼ T) \to ψ$
38	37	ex	$⊢ (φ \land (card (R) \in On \land card (R) \subseteq card (T)) \land \forall y (card (S) \in card (R) \to (S ≼ T \to χ))) \to (R ≼ T \to ψ)$
39	6	breq1d	$⊢ x = y \to (R ≼ T \leftrightarrow S ≼ T)$
40	39 4	imbi12d	$⊢ x = y \to ((R ≼ T \to ψ) \leftrightarrow (S ≼ T \to χ))$
41	7	breq1d	$⊢ x = A \to (R ≼ T \leftrightarrow T ≼ T)$
42	41 5	imbi12d	$⊢ x = A \to ((R ≼ T \to ψ) \leftrightarrow (T ≼ T \to θ))$
43	6	fveq2d	$⊢ x = y \to card (R) = card (S)$
44	7	fveq2d	$⊢ x = A \to card (R) = card (T)$
45	1 11 38 40 42 43 44	tfisi	$⊢ φ \to (T ≼ T \to θ)$
46	9 45	mpd	$⊢ φ \to θ$

Metamath Proof Explorer

Theorem indcardi

Proof