Theorem fin2so 37608

Description: Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)

Assertion

Ref	Expression
fin2so	⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Proof of Theorem fin2so

Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simplll 774	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2		ssrab2 4046	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥
3		sstr 3958	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
4	2, 3	mpan 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ⊆ 𝐴 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
5		elpw2g 5291	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ FinII → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴))
6	5	biimpar 477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ FinII ∧ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
7	4, 6	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
8	7	ralrimivw 3130	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9		vex 3454	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
10	9	rabex 5297	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
11	10	rgenw 3049	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
12		eqid 2730	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
13		eleq1 2817	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
14	12, 13	ralrnmptw 7069	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
15	11, 14	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
16	8, 15	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17		dfss3 3938	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
18	16, 17	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
19	18	adantlr 715	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
20	19	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
21	10, 12	dmmpti 6665	. . . . . . . . . . . . . . 15 ⊢ dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = 𝑥
22	21	neeq1i 2990	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23		dm0rn0 5891	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅)
24	23	necon3bii 2978	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
25	22, 24	sylbb1 237	. . . . . . . . . . . . 13 ⊢ (𝑥 ≠ ∅ → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
26	25	adantl 481	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
27		soss 5569	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or 𝑥))
28	27	impcom 407	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → 𝑅 Or 𝑥)
29		porpss 7706	. . . . . . . . . . . . . . . . 17 ⊢ [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
30	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑥 → [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
31		solin 5576	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣))
32		fin2solem 37607	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
33		breq2 5114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑦 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑦))
34	33	rabbidv 3416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
36		fin2solem 37607	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
37	36	ancom2s 650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
38	32, 35, 37	3orim123d 1446	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ((𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
39	31, 38	mpd 15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
40	39	ralrimivva 3181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Or 𝑥 → ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
41		breq1 5113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
42		eqeq1 2734	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
43		breq2 5114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
44	41, 42, 43	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ((𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
45	44	ralbidv 3157	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
46	12, 45	ralrnmptw 7069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
47	11, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
48	40, 47	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
49	48	r19.21bi 3230	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
50	9	rabex 5297	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
51	50	rgenw 3049	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
52	34	cbvmptv 5214	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑦 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
53		breq2 5114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
54		eqeq2 2742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 = 𝑧 ↔ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
55		breq1 5113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
56	53, 54, 55	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
57	52, 56	ralrnmptw 7069	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
58	51, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
59	49, 58	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
60	59	r19.21bi 3230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
61	60	anasss 466	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
62	30, 61	issod 5584	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Or 𝑥 → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
63	28, 62	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
64	63	adantll 714	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
65	64	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
66		fin2i2 10278	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ FinII ∧ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ∧ [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
67	1, 20, 26, 65, 66	syl22anc 838	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
68	52, 50	elrnmpti 5929	. . . . . . . . . . 11 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
69	67, 68	sylib 218	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
70		ssel2 3944	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
71		sonr 5573	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ 𝑧 ∈ 𝐴) → ¬ 𝑧𝑅𝑧)
72	70, 71	sylan2 593	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥)) → ¬ 𝑧𝑅𝑧)
73	72	anassrs 467	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
74	73	adantlr 715	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
75	74	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76		breq1 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑦 ↔ 𝑧𝑅𝑦))
77	76	elrab 3662	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑦))
78	77	simplbi2 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
80		vex 3454	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
81	80	elint2 4920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦)
82		eleq2 2818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
83	12, 82	ralrnmptw 7069	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
84	11, 83	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
85	81, 84	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
86		breq2 5114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑧 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑧))
87	86	rabbidv 3416	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})
88	87	eleq2d 2815	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
89	88	rspcv 3587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
90		breq1 5113	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑧 ↔ 𝑧𝑅𝑧))
91	90	elrab 3662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑧))
92	91	simprbi 496	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} → 𝑧𝑅𝑧)
93	89, 92	syl6 35	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
94	93	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
95	85, 94	biimtrid 242	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96		eleq2 2818	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
97	96	imbi1d 341	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
98	95, 97	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
99	98	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧))
100	79, 99	syld 47	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
101	100	adantlll 718	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
102	75, 101	mtod 198	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103	102	ex 412	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104	103	ralrimdva 3134	. . . . . . . . . . . . 13 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
105	104	reximdva 3147	. . . . . . . . . . . 12 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
106	105	adantll 714	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
107	106	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
108	69, 107	mpd 15	. . . . . . . . 9 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
109	108	expl 457	. . . . . . . 8 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
110	109	alrimiv 1927	. . . . . . 7 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
111		df-fr 5594	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
112	110, 111	sylibr 234	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113		simpr 484	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114		df-we 5596	. . . . . 6 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
115	112, 113, 114	sylanbrc 583	. . . . 5 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 We 𝐴)
116		weinxp 5726	. . . . 5 ⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117	115, 116	sylib 218	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118		sqxpexg 7734	. . . . . 6 ⊢ (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119		incom 4175	. . . . . . 7 ⊢ (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120		inex1g 5277	. . . . . . 7 ⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121	119, 120	eqeltrid 2833	. . . . . 6 ⊢ ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122		weeq1 5628	. . . . . . 7 ⊢ (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123	122	spcegv 3566	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124	118, 121, 123	3syl 18	. . . . 5 ⊢ (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125	124	imp 406	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126	117, 125	syldan 591	. . 3 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127		ween 9995	. . 3 ⊢ (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128	126, 127	sylibr 234	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129		fin23 10349	. . . . 5 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinIII)
130		fin34 10350	. . . . 5 ⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV)
131		fin45 10352	. . . . 5 ⊢ (𝐴 ∈ FinIV → 𝐴 ∈ FinV)
132	129, 130, 131	3syl 18	. . . 4 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinV)
133		fin56 10353	. . . 4 ⊢ (𝐴 ∈ FinV → 𝐴 ∈ FinVI)
134		fin67 10355	. . . 4 ⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII)
135	132, 133, 134	3syl 18	. . 3 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinVII)
136		fin71num 10357	. . . 4 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin))
137	136	biimpac 478	. . 3 ⊢ ((𝐴 ∈ FinVII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138	135, 137	sylan 580	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139	128, 138	syldan 591	1 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ w3o 1085  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054  {crab 3408  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  𝒫 cpw 4566  ∩ cint 4913   class class class wbr 5110   ↦ cmpt 5191   Po wpo 5547   Or wor 5548   Fr wfr 5591   We wwe 5593   × cxp 5639  dom cdm 5641  ran crn 5642   [⊊] crpss 7701  Fincfn 8921  cardccrd 9895  Fin^IIcfin2 10239  Fin^IVcfin4 10240  Fin^IIIcfin3 10241  Fin^Vcfin5 10242  Fin^VIcfin6 10243  Fin^VIIcfin7 10244

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-inf2 9601

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-se 5595  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-rpss 7702  df-om 7846  df-1st 7971  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-seqom 8419  df-1o 8437  df-2o 8438  df-er 8674  df-map 8804  df-en 8922  df-dom 8923  df-sdom 8924  df-fin 8925  df-oi 9470  df-wdom 9525  df-dju 9861  df-card 9899  df-fin2 10246  df-fin4 10247  df-fin3 10248  df-fin5 10249  df-fin6 10250  df-fin7 10251

This theorem is referenced by: (None)