Theorem fin2so 38510

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 787	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → 𝐴 ∈ FinII)
2		ssrab2 4028	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥
3		sstr 3939	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
4	2, 3	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ⊆ 𝐴 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
5		elpw2g 5295	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ FinII → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴))
6	5	biimpar 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ FinII ∧ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
7	4, 6	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
8	7	ralrimivw 3159	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9		vex 3455	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
10	9	rabex 5300	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
11	10	rgenw 3081	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
12		eqid 2761	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
13		eleq1 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
14	12, 13	ralrnmptw 7092	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
15	11, 14	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
16	8, 15	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17		dfss3 3920	. . . . . . . . . . . . . . 15 ⊢ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴 ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
18	16, 17	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
19	18	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
20	19	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴)
21	10, 12	dmmpti 6681	. . . . . . . . . . . . . . 15 ⊢ dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = 𝑥
22	21	neeq1i 3020	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23		dm0rn0 5906	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅)
24	23	necon3bii 3008	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
25	22, 24	sylbb1 240	. . . . . . . . . . . . 13 ⊢ (𝑥 ≠ ∅ → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
26	25	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
27		soss 5579	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or 𝑥))
28	27	impcom 413	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → 𝑅 Or 𝑥)
29		porpss 7741	. . . . . . . . . . . . . . . . 17 ⊢ [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
30	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑥 → [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
31		solin 5586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣))
32		fin2solem 38509	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
33		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑦 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑦))
34	33	rabbidv 3420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
36		fin2solem 38509	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
37	36	ancom2s 663	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑦𝑅𝑣 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
38	32, 35, 37	3orim123d 1472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ((𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
39	31, 38	mpd 16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
40	39	ralrimivva 3206	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Or 𝑥 → ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
41		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
42		eqeq1 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
43		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
44	41, 42, 43	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ((𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
45	44	ralbidv 3186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
46	12, 45	ralrnmptw 7092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
47	11, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
48	40, 47	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
49	48	r19.21bi 3255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
50	9	rabex 5300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
51	50	rgenw 3081	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
52	34	cbvmptv 5209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑦 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
53		breq2 5107	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
54		eqeq2 2773	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 = 𝑧 ↔ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
55		breq1 5106	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
56	53, 54, 55	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
57	52, 56	ralrnmptw 7092	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
58	51, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
59	49, 58	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
60	59	r19.21bi 3255	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
61	60	anasss 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
62	30, 61	issod 5594	. . . . . . . . . . . . . . 15 ⊢ (𝑅 Or 𝑥 → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
63	28, 62	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
64	63	adantll 727	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
65	64	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
66		fin2i2 10389	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ FinII ∧ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ⊆ 𝒫 𝐴) ∧ (ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ∧ [⊊] Or ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
67	1, 20, 26, 65, 66	syl22anc 852	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
68	52, 50	elrnmpti 5944	. . . . . . . . . . 11 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
69	67, 68	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
70		ssel2 3926	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
71		sonr 5583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Or 𝐴 ∧ 𝑧 ∈ 𝐴) → ¬ 𝑧𝑅𝑧)
72	70, 71	sylan2 605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥)) → ¬ 𝑧𝑅𝑧)
73	72	anassrs 473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
74	73	adantlr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → ¬ 𝑧𝑅𝑧)
75	74	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑧)
76		breq1 5106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑦 ↔ 𝑧𝑅𝑦))
77	76	elrab 3645	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑦))
78	77	simplbi2 506	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
79	78	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
80		vex 3455	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
81	80	elint2 4914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦)
82		eleq2 2850	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
83	12, 82	ralrnmptw 7092	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
84	11, 83	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
85	81, 84	bitri 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
86		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑧 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑧))
87	86	rabbidv 3420	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})
88	87	eleq2d 2847	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
89	88	rspcv 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
90		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑧 ↔ 𝑧𝑅𝑧))
91	90	elrab 3645	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑧))
92	91	simprbi 503	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧} → 𝑧𝑅𝑧)
93	89, 92	syl6 36	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
94	93	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧𝑅𝑧))
95	85, 94	biimtrid 245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧))
96		eleq2 2850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
97	96	imbi1d 344	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) → 𝑧𝑅𝑧) ↔ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
98	95, 97	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧)))
99	98	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → 𝑧𝑅𝑧))
100	79, 99	syld 48	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
101	100	adantlll 731	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧𝑅𝑧))
102	75, 101	mtod 201	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → ¬ 𝑧𝑅𝑦)
103	102	ex 418	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ¬ 𝑧𝑅𝑦))
104	103	ralrimdva 3163	. . . . . . . . . . . . 13 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
105	104	reximdva 3176	. . . . . . . . . . . 12 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
106	105	adantll 727	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
107	106	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → (∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
108	69, 107	mpd 16	. . . . . . . . 9 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
109	108	expl 463	. . . . . . . 8 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
110	109	alrimiv 1960	. . . . . . 7 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
111		df-fr 5604	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
112	110, 111	sylibr 237	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113		simpr 490	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114		df-we 5606	. . . . . 6 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
115	112, 113, 114	sylanbrc 595	. . . . 5 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 We 𝐴)
116		weinxp 5736	. . . . 5 ⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117	115, 116	sylib 221	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118		sqxpexg 7767	. . . . . 6 ⊢ (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119		incom 4155	. . . . . . 7 ⊢ (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120		inex1g 5279	. . . . . . 7 ⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121	119, 120	eqeltrid 2865	. . . . . 6 ⊢ ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122		weeq1 5638	. . . . . . 7 ⊢ (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123	122	spcegv 3552	. . . . . 6 ⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∈ V → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
124	118, 121, 123	3syl 19	. . . . 5 ⊢ (𝐴 ∈ FinII → ((𝑅 ∩ (𝐴 × 𝐴)) We 𝐴 → ∃𝑧 𝑧 We 𝐴))
125	124	imp 412	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴) → ∃𝑧 𝑧 We 𝐴)
126	117, 125	syldan 603	. . 3 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → ∃𝑧 𝑧 We 𝐴)
127		ween 10107	. . 3 ⊢ (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128	126, 127	sylibr 237	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129		fin23 10460	. . . . 5 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinIII)
130		fin34 10461	. . . . 5 ⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV)
131		fin45 10463	. . . . 5 ⊢ (𝐴 ∈ FinIV → 𝐴 ∈ FinV)
132	129, 130, 131	3syl 19	. . . 4 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinV)
133		fin56 10464	. . . 4 ⊢ (𝐴 ∈ FinV → 𝐴 ∈ FinVI)
134		fin67 10466	. . . 4 ⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII)
135	132, 133, 134	3syl 19	. . 3 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinVII)
136		fin71num 10468	. . . 4 ⊢ (𝐴 ∈ dom card → (𝐴 ∈ FinVII ↔ 𝐴 ∈ Fin))
137	136	biimpac 484	. . 3 ⊢ ((𝐴 ∈ FinVII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
138	135, 137	sylan 592	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝐴 ∈ dom card) → 𝐴 ∈ Fin)
139	128, 138	syldan 603	1 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ w3o 1102  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  {crab 3413  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899  ∅c0 4279  𝒫 cpw 4557  ∩ cint 4907   class class class wbr 5103   ↦ cmpt 5186   Po wpo 5557   Or wor 5558   Fr wfr 5601   We wwe 5603   × cxp 5649  dom cdm 5651  ran crn 5652   [⊊] crpss 7736  Fincfn 8966  cardccrd 10009  Fin^IIcfin2 10350  Fin^IVcfin4 10351  Fin^IIIcfin3 10352  Fin^Vcfin5 10353  Fin^VIcfin6 10354  Fin^VIIcfin7 10355

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-rpss 7737  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-seqom 8451  df-1o 8469  df-2o 8470  df-er 8710  df-map 8842  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-oi 9497  df-wdom 9552  df-dju 9975  df-card 10013  df-fin2 10357  df-fin4 10358  df-fin3 10359  df-fin5 10360  df-fin6 10361  df-fin7 10362

This theorem is used by: (None)