Theorem cardprclem

Description: Lemma for cardprc . (Contributed by Mario Carneiro, 22-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

	Ref	Expression
Hypothesis	cardprclem.1	⊢ 𝐴 = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
Assertion	cardprclem	⊢ ¬ 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		cardprclem.1	⊢ 𝐴 = { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 }
2	1	eleq2i	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } )
3		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ ( card ‘ 𝑥 ) = 𝑥 } ↔ ( card ‘ 𝑥 ) = 𝑥 )
4		iscard	⊢ ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≺ 𝑥 ) )
5	2 3 4	3bitri	⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ≺ 𝑥 ) )
6	5	simplbi	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On )
7	6	ssriv	⊢ 𝐴 ⊆ On
8		ssonuni	⊢ ( 𝐴 ∈ V → ( 𝐴 ⊆ On → ∪ 𝐴 ∈ On ) )
9	7 8	mpi	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ∈ On )
10		domrefg	⊢ ( ∪ 𝐴 ∈ On → ∪ 𝐴 ≼ ∪ 𝐴 )
11	9 10	syl	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ≼ ∪ 𝐴 )
12		elharval	⊢ ( ∪ 𝐴 ∈ ( har ‘ ∪ 𝐴 ) ↔ ( ∪ 𝐴 ∈ On ∧ ∪ 𝐴 ≼ ∪ 𝐴 ) )
13	9 11 12	sylanbrc	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ∈ ( har ‘ ∪ 𝐴 ) )
14	7	sseli	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ On )
15		domrefg	⊢ ( 𝑧 ∈ On → 𝑧 ≼ 𝑧 )
16	15	ancli	⊢ ( 𝑧 ∈ On → ( 𝑧 ∈ On ∧ 𝑧 ≼ 𝑧 ) )
17		elharval	⊢ ( 𝑧 ∈ ( har ‘ 𝑧 ) ↔ ( 𝑧 ∈ On ∧ 𝑧 ≼ 𝑧 ) )
18	16 17	sylibr	⊢ ( 𝑧 ∈ On → 𝑧 ∈ ( har ‘ 𝑧 ) )
19	14 18	syl	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( har ‘ 𝑧 ) )
20		harcard	⊢ ( card ‘ ( har ‘ 𝑧 ) ) = ( har ‘ 𝑧 )
21		fvex	⊢ ( har ‘ 𝑧 ) ∈ V
22		fveq2	⊢ ( 𝑥 = ( har ‘ 𝑧 ) → ( card ‘ 𝑥 ) = ( card ‘ ( har ‘ 𝑧 ) ) )
23		id	⊢ ( 𝑥 = ( har ‘ 𝑧 ) → 𝑥 = ( har ‘ 𝑧 ) )
24	22 23	eqeq12d	⊢ ( 𝑥 = ( har ‘ 𝑧 ) → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ ( har ‘ 𝑧 ) ) = ( har ‘ 𝑧 ) ) )
25	21 24 1	elab2	⊢ ( ( har ‘ 𝑧 ) ∈ 𝐴 ↔ ( card ‘ ( har ‘ 𝑧 ) ) = ( har ‘ 𝑧 ) )
26	20 25	mpbir	⊢ ( har ‘ 𝑧 ) ∈ 𝐴
27		eleq2	⊢ ( 𝑤 = ( har ‘ 𝑧 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( har ‘ 𝑧 ) ) )
28		eleq1	⊢ ( 𝑤 = ( har ‘ 𝑧 ) → ( 𝑤 ∈ 𝐴 ↔ ( har ‘ 𝑧 ) ∈ 𝐴 ) )
29	27 28	anbi12d	⊢ ( 𝑤 = ( har ‘ 𝑧 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) ↔ ( 𝑧 ∈ ( har ‘ 𝑧 ) ∧ ( har ‘ 𝑧 ) ∈ 𝐴 ) ) )
30	21 29	spcev	⊢ ( ( 𝑧 ∈ ( har ‘ 𝑧 ) ∧ ( har ‘ 𝑧 ) ∈ 𝐴 ) → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) )
31	19 26 30	sylancl	⊢ ( 𝑧 ∈ 𝐴 → ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) )
32		eluni	⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝐴 ) )
33	31 32	sylibr	⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴 )
34	33	ssriv	⊢ 𝐴 ⊆ ∪ 𝐴
35		harcard	⊢ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 )
36		fvex	⊢ ( har ‘ ∪ 𝐴 ) ∈ V
37		fveq2	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → ( card ‘ 𝑥 ) = ( card ‘ ( har ‘ ∪ 𝐴 ) ) )
38		id	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → 𝑥 = ( har ‘ ∪ 𝐴 ) )
39	37 38	eqeq12d	⊢ ( 𝑥 = ( har ‘ ∪ 𝐴 ) → ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 ) ) )
40	36 39 1	elab2	⊢ ( ( har ‘ ∪ 𝐴 ) ∈ 𝐴 ↔ ( card ‘ ( har ‘ ∪ 𝐴 ) ) = ( har ‘ ∪ 𝐴 ) )
41	35 40	mpbir	⊢ ( har ‘ ∪ 𝐴 ) ∈ 𝐴
42	34 41	sselii	⊢ ( har ‘ ∪ 𝐴 ) ∈ ∪ 𝐴
43	13 42	jctir	⊢ ( 𝐴 ∈ V → ( ∪ 𝐴 ∈ ( har ‘ ∪ 𝐴 ) ∧ ( har ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ) )
44		eloni	⊢ ( ∪ 𝐴 ∈ On → Ord ∪ 𝐴 )
45		ordn2lp	⊢ ( Ord ∪ 𝐴 → ¬ ( ∪ 𝐴 ∈ ( har ‘ ∪ 𝐴 ) ∧ ( har ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ) )
46	9 44 45	3syl	⊢ ( 𝐴 ∈ V → ¬ ( ∪ 𝐴 ∈ ( har ‘ ∪ 𝐴 ) ∧ ( har ‘ ∪ 𝐴 ) ∈ ∪ 𝐴 ) )
47	43 46	pm2.65i	⊢ ¬ 𝐴 ∈ V