Theorem fin2so 38291

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 4035	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥
3		sstr 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝑥 ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
4	2, 3	mpan 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ⊆ 𝐴 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴)
5		elpw2g 5306	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ FinII → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴))
6	5	biimpar 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ FinII ∧ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
7	4, 6	sylan2 605	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
8	7	ralrimivw 3163	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
9		vex 3461	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑥 ∈ V
10	9	rabex 5311	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
11	10	rgenw 3085	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V
12		eqid 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
13		eleq1 2853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑦 ∈ 𝒫 𝐴 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
14	12, 13	ralrnmptw 7093	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴))
15	11, 14	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴 ↔ ∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ 𝒫 𝐴)
16	8, 15	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝐴) → ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑦 ∈ 𝒫 𝐴)
17		dfss3 3927	. . . . . . . . . . . . . . 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 6683	. . . . . . . . . . . . . . 15 ⊢ dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = 𝑥
22	21	neeq1i 3024	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ 𝑥 ≠ ∅)
23		dm0rn0 5916	. . . . . . . . . . . . . . 15 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = ∅)
24	23	necon3bii 3012	. . . . . . . . . . . . . 14 ⊢ (dom (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅ ↔ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
25	22, 24	sylbb1 240	. . . . . . . . . . . . 13 ⊢ (𝑥 ≠ ∅ → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
26	25	adantl 487	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ≠ ∅)
27		soss 5591	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ⊆ 𝐴 → (𝑅 Or 𝐴 → 𝑅 Or 𝑥))
28	27	impcom 413	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) → 𝑅 Or 𝑥)
29		porpss 7730	. . . . . . . . . . . . . . . . 17 ⊢ [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
30	29	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 Or 𝑥 → [⊊] Po ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
31		solin 5598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 ∨ 𝑣 = 𝑦 ∨ 𝑦𝑅𝑣))
32		fin2solem 38290	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣𝑅𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
33		breq2 5115	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑦 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑦))
34	33	rabbidv 3425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Or 𝑥 ∧ (𝑣 ∈ 𝑥 ∧ 𝑦 ∈ 𝑥)) → (𝑣 = 𝑦 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
36		fin2solem 38290	. . . . . . . . . . . . . . . . . . . . . . . . 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 3210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 Or 𝑥 → ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
41		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
42		eqeq1 2769	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
43		breq2 5115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
44	41, 42, 43	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → ((𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
45	44	ralbidv 3190	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
46	12, 45	ralrnmptw 7093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})))
47	11, 46	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢) ↔ ∀𝑣 ∈ 𝑥 ∀𝑦 ∈ 𝑥 ({𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
48	40, 47	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑅 Or 𝑥 → ∀𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
49	48	r19.21bi 3259	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
50	9	rabex 5311	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
51	50	rgenw 3085	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V
52	34	cbvmptv 5217	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = (𝑦 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
53		breq2 5115	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 [⊊] 𝑧 ↔ 𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
54		eqeq2 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑢 = 𝑧 ↔ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
55		breq1 5114	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → (𝑧 [⊊] 𝑢 ↔ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
56	53, 54, 55	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ((𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
57	52, 56	ralrnmptw 7093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∈ V → (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢)))
58	51, 57	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢) ↔ ∀𝑦 ∈ 𝑥 (𝑢 [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ 𝑢 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ∨ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] 𝑢))
59	49, 58	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → ∀𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})(𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
60	59	r19.21bi 3259	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 Or 𝑥 ∧ 𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
61	60	anasss 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 Or 𝑥 ∧ (𝑢 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∧ 𝑧 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))) → (𝑢 [⊊] 𝑧 ∨ 𝑢 = 𝑧 ∨ 𝑧 [⊊] 𝑢))
62	30, 61	issod 5606	. . . . . . . . . . . . . . 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 10313	. . . . . . . . . . . 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 5954	. . . . . . . . . . 11 ⊢ (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
69	67, 68	sylib 221	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) ∧ 𝑥 ⊆ 𝐴) ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦})
70		ssel2 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝐴)
71		sonr 5595	. . . . . . . . . . . . . . . . . . . 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 5114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑦 ↔ 𝑧𝑅𝑦))
77	76	elrab 3652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} ↔ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑦))
78	77	simplbi2 506	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ 𝑥 → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
79	78	ad2antlr 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥) ∧ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}) → (𝑧𝑅𝑦 → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦}))
80		vex 3461	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑧 ∈ V
81	80	elint2 4921	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦)
82		eleq2 2854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
83	12, 82	ralrnmptw 7093	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑣 ∈ 𝑥 {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ∈ V → (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}))
84	11, 83	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑦 ∈ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})𝑧 ∈ 𝑦 ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
85	81, 84	bitri 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ ∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) ↔ ∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣})
86		breq2 5115	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑣 = 𝑧 → (𝑤𝑅𝑣 ↔ 𝑤𝑅𝑧))
87	86	rabbidv 3425	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑣 = 𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})
88	87	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑣 = 𝑧 → (𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} ↔ 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
89	88	rspcv 3579	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 ∈ 𝑥 → (∀𝑣 ∈ 𝑥 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣} → 𝑧 ∈ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
90		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = 𝑧 → (𝑤𝑅𝑧 ↔ 𝑧𝑅𝑧))
91	90	elrab 3652	. . . . . . . . . . . . . . . . . . . . . . . 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 2854	. . . . . . . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . 13 ⊢ (((𝑅 Or 𝐴 ∧ 𝑥 ⊆ 𝐴) ∧ 𝑦 ∈ 𝑥) → (∩ ran (𝑣 ∈ 𝑥 ↦ {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑣}) = {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} → ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
105	104	reximdva 3180	. . . . . . . . . . . 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 5616	. . . . . . 7 ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))
112	110, 111	sylibr 237	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Fr 𝐴)
113		simpr 490	. . . . . 6 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 Or 𝐴)
114		df-we 5618	. . . . . 6 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
115	112, 113, 114	sylanbrc 595	. . . . 5 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝑅 We 𝐴)
116		weinxp 5748	. . . . 5 ⊢ (𝑅 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
117	115, 116	sylib 221	. . . 4 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴)
118		sqxpexg 7756	. . . . . 6 ⊢ (𝐴 ∈ FinII → (𝐴 × 𝐴) ∈ V)
119		incom 4162	. . . . . . 7 ⊢ (𝑅 ∩ (𝐴 × 𝐴)) = ((𝐴 × 𝐴) ∩ 𝑅)
120		inex1g 5290	. . . . . . 7 ⊢ ((𝐴 × 𝐴) ∈ V → ((𝐴 × 𝐴) ∩ 𝑅) ∈ V)
121	119, 120	eqeltrid 2869	. . . . . 6 ⊢ ((𝐴 × 𝐴) ∈ V → (𝑅 ∩ (𝐴 × 𝐴)) ∈ V)
122		weeq1 5650	. . . . . . 7 ⊢ (𝑧 = (𝑅 ∩ (𝐴 × 𝐴)) → (𝑧 We 𝐴 ↔ (𝑅 ∩ (𝐴 × 𝐴)) We 𝐴))
123	122	spcegv 3558	. . . . . 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 10031	. . 3 ⊢ (𝐴 ∈ dom card ↔ ∃𝑧 𝑧 We 𝐴)
128	126, 127	sylibr 237	. 2 ⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ dom card)
129		fin23 10384	. . . . 5 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinIII)
130		fin34 10385	. . . . 5 ⊢ (𝐴 ∈ FinIII → 𝐴 ∈ FinIV)
131		fin45 10387	. . . . 5 ⊢ (𝐴 ∈ FinIV → 𝐴 ∈ FinV)
132	129, 130, 131	3syl 19	. . . 4 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinV)
133		fin56 10388	. . . 4 ⊢ (𝐴 ∈ FinV → 𝐴 ∈ FinVI)
134		fin67 10390	. . . 4 ⊢ (𝐴 ∈ FinVI → 𝐴 ∈ FinVII)
135	132, 133, 134	3syl 19	. . 3 ⊢ (𝐴 ∈ FinII → 𝐴 ∈ FinVII)
136		fin71num 10392	. . . 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 2146   ≠ wne 2960  ∀wral 3081  ∃wrex 3091  {crab 3418  Vcvv 3457   ∩ cin 3905   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  ∩ cint 4914   class class class wbr 5111   ↦ cmpt 5194   Po wpo 5569   Or wor 5570   Fr wfr 5613   We wwe 5615   × cxp 5661  dom cdm 5663  ran crn 5664   [⊊] crpss 7725  Fincfn 8945  cardccrd 9933  Fin^IIcfin2 10274  Fin^IVcfin4 10275  Fin^IIIcfin3 10276  Fin^Vcfin5 10277  Fin^VIcfin6 10278  Fin^VIIcfin7 10279

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-inf2 9613

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rmo 3371  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-int 4915  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-rpss 7726  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-seqom 8437  df-1o 8455  df-2o 8456  df-er 8696  df-map 8828  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-oi 9475  df-wdom 9530  df-dju 9899  df-card 9937  df-fin2 10281  df-fin4 10282  df-fin3 10283  df-fin5 10284  df-fin6 10285  df-fin7 10286

This theorem is used by: (None)